; benchmark generated from python API
(set-info :status unknown)
(declare-fun back_to_top_feasible () Bool)
(declare-fun video_3_body_feasible () Bool)
(declare-fun video_3_title_feasible () Bool)
(declare-fun video_2_body_feasible () Bool)
(declare-fun video_2_title_feasible () Bool)
(declare-fun video_1_body_feasible () Bool)
(declare-fun video_1_title_feasible () Bool)
(declare-fun video_3_feasible () Bool)
(declare-fun video_2_feasible () Bool)
(declare-fun video_1_feasible () Bool)
(declare-fun homes_kid_3_feasible () Bool)
(declare-fun homes_feasible () Bool)
(declare-fun homes_kid_2_feasible () Bool)
(declare-fun homes_kid_1_feasible () Bool)
(declare-fun homes_kid_0_feasible () Bool)
(declare-fun menus_kid_1_feasible () Bool)
(declare-fun menus_feasible () Bool)
(declare-fun menus_kid_0_feasible () Bool)
(declare-fun ads_top_2_feasible () Bool)
(declare-fun ads_top_1_kid_4_feasible () Bool)
(declare-fun ads_top_1_feasible () Bool)
(declare-fun categories_feasible () Bool)
(declare-fun store_feasible () Bool)
(declare-fun home_feasible () Bool)
(declare-fun prime_top_feasible () Bool)
(declare-fun left_buttons_detail_feasible () Bool)
(declare-fun ads_pics_feasible () Bool)
(declare-fun left_buttons_watch_feasible () Bool)
(declare-fun ads_pics_2_feasible () Bool)
(declare-fun left_buttons_title_feasible () Bool)
(declare-fun ads_pics_holder_feasible () Bool)
(declare-fun ads_top_holder_feasible () Bool)
(declare-fun search_bar_kid_1_feasible () Bool)
(declare-fun search_bar_kid_0_feasible () Bool)
(declare-fun search_kid_6_feasible () Bool)
(declare-fun search_kid_5_feasible () Bool)
(declare-fun search_kid_4_feasible () Bool)
(declare-fun search_kid_3_feasible () Bool)
(declare-fun search_bar_feasible () Bool)
(declare-fun search_kid_1_feasible () Bool)
(declare-fun search_kid_0_feasible () Bool)
(declare-fun buttons_feasible () Bool)
(declare-fun search_feasible () Bool)
(declare-fun info_feasible () Bool)
(declare-fun mainbody_feasible () Bool)
(declare-fun ads_feasible () Bool)
(declare-fun title_feasible () Bool)
(declare-fun back_ground_feasible () Bool)
(declare-fun back_to_top_width () Real)
(declare-fun back_to_top_x () Real)
(declare-fun info_width () Real)
(declare-fun info_x () Real)
(declare-fun info_hight () Real)
(declare-fun back_to_top_hight () Real)
(declare-fun info_y () Real)
(declare-fun back_to_top_y () Real)
(declare-fun video_3_body_kid_6_width () Real)
(declare-fun video_3_body_width () Real)
(declare-fun video_3_body_kid_6_x () Real)
(declare-fun video_3_body_x () Real)
(declare-fun video_3_body_kid_6_feasible () Bool)
(declare-fun video_3_body_kid_5_width () Real)
(declare-fun video_3_body_kid_5_x () Real)
(declare-fun video_3_body_kid_5_feasible () Bool)
(declare-fun video_3_body_kid_4_width () Real)
(declare-fun video_3_body_kid_4_x () Real)
(declare-fun video_3_body_kid_4_feasible () Bool)
(declare-fun video_3_body_kid_3_width () Real)
(declare-fun video_3_body_kid_3_x () Real)
(declare-fun video_3_body_kid_3_feasible () Bool)
(declare-fun video_3_body_kid_2_width () Real)
(declare-fun video_3_body_kid_2_x () Real)
(declare-fun video_3_body_kid_2_feasible () Bool)
(declare-fun video_3_body_kid_1_x () Real)
(declare-fun video_3_body_kid_1_width () Real)
(declare-fun video_3_body_kid_1_feasible () Bool)
(declare-fun video_3_body_kid_0_x () Real)
(declare-fun video_3_body_kid_0_width () Real)
(declare-fun video_3_body_kid_0_feasible () Bool)
(declare-fun video_3_body_kid_6_y () Real)
(declare-fun video_3_body_y () Real)
(declare-fun video_3_body_kid_6_hight () Real)
(declare-fun video_3_body_hight () Real)
(declare-fun video_3_body_kid_5_y () Real)
(declare-fun video_3_body_kid_5_hight () Real)
(declare-fun video_3_body_kid_4_y () Real)
(declare-fun video_3_body_kid_4_hight () Real)
(declare-fun video_3_body_kid_3_y () Real)
(declare-fun video_3_body_kid_3_hight () Real)
(declare-fun video_3_body_kid_2_y () Real)
(declare-fun video_3_body_kid_2_hight () Real)
(declare-fun video_3_body_kid_1_y () Real)
(declare-fun video_3_body_kid_1_hight () Real)
(declare-fun video_3_body_kid_0_hight () Real)
(declare-fun video_3_body_kid_0_y () Real)
(declare-fun video_3_width () Real)
(declare-fun video_3_x () Real)
(declare-fun video_3_title_hight () Real)
(declare-fun video_3_title_width () Real)
(declare-fun video_3_hight () Real)
(declare-fun video_3_y () Real)
(declare-fun video_3_title_y () Real)
(declare-fun video_3_title_x () Real)
(declare-fun video_2_body_kid_6_width () Real)
(declare-fun video_2_body_width () Real)
(declare-fun video_2_body_kid_6_x () Real)
(declare-fun video_2_body_x () Real)
(declare-fun video_2_body_kid_6_feasible () Bool)
(declare-fun video_2_body_kid_5_width () Real)
(declare-fun video_2_body_kid_5_x () Real)
(declare-fun video_2_body_kid_5_feasible () Bool)
(declare-fun video_2_body_kid_4_width () Real)
(declare-fun video_2_body_kid_4_x () Real)
(declare-fun video_2_body_kid_4_feasible () Bool)
(declare-fun video_2_body_kid_3_x () Real)
(declare-fun video_2_body_kid_3_width () Real)
(declare-fun video_2_body_kid_3_feasible () Bool)
(declare-fun video_2_body_kid_2_x () Real)
(declare-fun video_2_body_kid_2_width () Real)
(declare-fun video_2_body_kid_2_feasible () Bool)
(declare-fun video_2_body_kid_1_width () Real)
(declare-fun video_2_body_kid_1_x () Real)
(declare-fun video_2_body_kid_1_feasible () Bool)
(declare-fun video_2_body_kid_0_width () Real)
(declare-fun video_2_body_kid_0_x () Real)
(declare-fun video_2_body_kid_0_feasible () Bool)
(declare-fun video_2_body_kid_6_y () Real)
(declare-fun video_2_body_y () Real)
(declare-fun video_2_body_kid_6_hight () Real)
(declare-fun video_2_body_hight () Real)
(declare-fun video_2_body_kid_5_y () Real)
(declare-fun video_2_body_kid_5_hight () Real)
(declare-fun video_2_body_kid_4_y () Real)
(declare-fun video_2_body_kid_4_hight () Real)
(declare-fun video_2_body_kid_3_y () Real)
(declare-fun video_2_body_kid_3_hight () Real)
(declare-fun video_2_body_kid_2_y () Real)
(declare-fun video_2_body_kid_2_hight () Real)
(declare-fun video_2_body_kid_1_y () Real)
(declare-fun video_2_body_kid_1_hight () Real)
(declare-fun video_2_body_kid_0_hight () Real)
(declare-fun video_2_body_kid_0_y () Real)
(declare-fun video_2_width () Real)
(declare-fun video_2_x () Real)
(declare-fun video_2_title_hight () Real)
(declare-fun video_2_title_width () Real)
(declare-fun video_2_y () Real)
(declare-fun video_2_hight () Real)
(declare-fun video_2_title_y () Real)
(declare-fun video_2_title_x () Real)
(declare-fun video_1_body_kid_6_width () Real)
(declare-fun video_1_body_x () Real)
(declare-fun video_1_body_kid_6_x () Real)
(declare-fun video_1_body_width () Real)
(declare-fun video_1_body_kid_6_feasible () Bool)
(declare-fun video_1_body_kid_5_x () Real)
(declare-fun video_1_body_kid_5_width () Real)
(declare-fun video_1_body_kid_5_feasible () Bool)
(declare-fun video_1_body_kid_4_x () Real)
(declare-fun video_1_body_kid_4_width () Real)
(declare-fun video_1_body_kid_4_feasible () Bool)
(declare-fun video_1_body_kid_3_width () Real)
(declare-fun video_1_body_kid_3_x () Real)
(declare-fun video_1_body_kid_3_feasible () Bool)
(declare-fun video_1_body_kid_2_width () Real)
(declare-fun video_1_body_kid_2_x () Real)
(declare-fun video_1_body_kid_2_feasible () Bool)
(declare-fun video_1_body_kid_1_width () Real)
(declare-fun video_1_body_kid_1_x () Real)
(declare-fun video_1_body_kid_1_feasible () Bool)
(declare-fun video_1_body_kid_0_width () Real)
(declare-fun video_1_body_kid_0_x () Real)
(declare-fun video_1_body_kid_0_feasible () Bool)
(declare-fun video_1_body_y () Real)
(declare-fun video_1_body_kid_6_y () Real)
(declare-fun video_1_body_hight () Real)
(declare-fun video_1_body_kid_6_hight () Real)
(declare-fun video_1_body_kid_5_y () Real)
(declare-fun video_1_body_kid_5_hight () Real)
(declare-fun video_1_body_kid_4_y () Real)
(declare-fun video_1_body_kid_4_hight () Real)
(declare-fun video_1_body_kid_3_y () Real)
(declare-fun video_1_body_kid_3_hight () Real)
(declare-fun video_1_body_kid_2_y () Real)
(declare-fun video_1_body_kid_2_hight () Real)
(declare-fun video_1_body_kid_1_y () Real)
(declare-fun video_1_body_kid_1_hight () Real)
(declare-fun video_1_body_kid_0_hight () Real)
(declare-fun video_1_body_kid_0_y () Real)
(declare-fun video_1_width () Real)
(declare-fun video_1_x () Real)
(declare-fun video_1_title_hight () Real)
(declare-fun video_1_title_width () Real)
(declare-fun video_1_hight () Real)
(declare-fun video_1_y () Real)
(declare-fun video_1_title_y () Real)
(declare-fun video_1_title_x () Real)
(declare-fun mainbody_y () Real)
(declare-fun mainbody_hight () Real)
(declare-fun mainbody_width () Real)
(declare-fun mainbody_x () Real)
(declare-fun homes_kid_2_width () Real)
(declare-fun homes_kid_2_x () Real)
(declare-fun homes_kid_3_x () Real)
(declare-fun homes_kid_1_x () Real)
(declare-fun homes_kid_1_width () Real)
(declare-fun homes_kid_0_x () Real)
(declare-fun homes_kid_0_width () Real)
(declare-fun homes_x () Real)
(declare-fun homes_kid_3_y () Real)
(declare-fun homes_kid_3_hight () Real)
(declare-fun homes_hight () Real)
(declare-fun homes_y () Real)
(declare-fun homes_kid_2_hight () Real)
(declare-fun homes_kid_2_y () Real)
(declare-fun homes_kid_1_hight () Real)
(declare-fun homes_kid_1_y () Real)
(declare-fun homes_kid_0_hight () Real)
(declare-fun homes_kid_0_y () Real)
(declare-fun homes_kid_3_width () Real)
(declare-fun homes_width () Real)
(declare-fun menus_kid_0_width () Real)
(declare-fun menus_kid_1_width () Real)
(declare-fun menus_kid_1_x () Real)
(declare-fun menus_width () Real)
(declare-fun menus_x () Real)
(declare-fun menus_kid_0_x () Real)
(declare-fun menus_kid_1_hight () Real)
(declare-fun menus_kid_1_y () Real)
(declare-fun menus_hight () Real)
(declare-fun menus_y () Real)
(declare-fun menus_kid_0_y () Real)
(declare-fun menus_kid_0_hight () Real)
(declare-fun ads_top_2_width () Real)
(declare-fun ads_width () Real)
(declare-fun ads_top_2_x () Real)
(declare-fun ads_x () Real)
(declare-fun ads_top_2_hight () Real)
(declare-fun ads_top_2_y () Real)
(declare-fun prime_top_width () Real)
(declare-fun ads_top_1_kid_4_width () Real)
(declare-fun categories_width () Real)
(declare-fun store_width () Real)
(declare-fun home_width () Real)
(declare-fun ads_top_1_hight () Real)
(declare-fun ads_top_1_width () Real)
(declare-fun ads_top_1_x () Real)
(declare-fun categories_x () Real)
(declare-fun ads_top_1_kid_4_x () Real)
(declare-fun store_x () Real)
(declare-fun home_x () Real)
(declare-fun prime_top_x () Real)
(declare-fun ads_top_1_kid_4_hight () Real)
(declare-fun ads_top_1_kid_4_y () Real)
(declare-fun ads_top_1_y () Real)
(declare-fun categories_hight () Real)
(declare-fun categories_y () Real)
(declare-fun store_hight () Real)
(declare-fun store_y () Real)
(declare-fun home_hight () Real)
(declare-fun home_y () Real)
(declare-fun prime_top_y () Real)
(declare-fun prime_top_hight () Real)
(declare-fun ads_top_holder_hight () Real)
(declare-fun ads_top_holder_y () Real)
(declare-fun ads_top_holder_width () Real)
(declare-fun ads_top_holder_x () Real)
(declare-fun ads_pics_2_y () Real)
(declare-fun left_buttons_watch_hight () Real)
(declare-fun left_buttons_watch_y () Real)
(declare-fun ads_pics_2_hight () Real)
(declare-fun left_buttons_title_hight () Real)
(declare-fun left_buttons_title_y () Real)
(declare-fun left_buttons_watch_x () Real)
(declare-fun ads_pics_2_x () Real)
(declare-fun left_buttons_title_x () Real)
(declare-fun ads_pics_2_width () Real)
(declare-fun left_buttons_watch_width () Real)
(declare-fun left_buttons_title_width () Real)
(declare-fun left_buttons_detail_y () Real)
(declare-fun left_buttons_detail_hight () Real)
(declare-fun left_buttons_detail_width () Real)
(declare-fun ads_pics_holder_width () Real)
(declare-fun left_buttons_detail_x () Real)
(declare-fun ads_pics_x () Real)
(declare-fun ads_pics_hight () Real)
(declare-fun ads_pics_y () Real)
(declare-fun ads_pics_width () Real)
(declare-fun ads_pics_holder_hight () Real)
(declare-fun ads_pics_holder_x () Real)
(declare-fun ads_pics_3_feasible () Bool)
(declare-fun ads_pics_3_hight () Real)
(declare-fun ads_pics_3_y () Real)
(declare-fun ads_pics_holder_y () Real)
(declare-fun ads_pics_3_width () Real)
(declare-fun ads_pics_3_x () Real)
(declare-fun ads_hight () Real)
(declare-fun ads_y () Real)
(declare-fun buttons_kid_16_x () Real)
(declare-fun buttons_x () Real)
(declare-fun buttons_kid_16_width () Real)
(declare-fun buttons_width () Real)
(declare-fun buttons_kid_16_feasible () Bool)
(declare-fun buttons_kid_15_width () Real)
(declare-fun buttons_kid_15_x () Real)
(declare-fun buttons_kid_15_feasible () Bool)
(declare-fun buttons_kid_14_width () Real)
(declare-fun buttons_kid_14_x () Real)
(declare-fun buttons_kid_14_feasible () Bool)
(declare-fun buttons_kid_13_width () Real)
(declare-fun buttons_kid_13_x () Real)
(declare-fun buttons_kid_13_feasible () Bool)
(declare-fun buttons_kid_12_width () Real)
(declare-fun buttons_kid_12_x () Real)
(declare-fun buttons_kid_12_feasible () Bool)
(declare-fun buttons_kid_11_x () Real)
(declare-fun buttons_kid_11_width () Real)
(declare-fun buttons_kid_11_feasible () Bool)
(declare-fun buttons_kid_10_width () Real)
(declare-fun buttons_kid_10_x () Real)
(declare-fun buttons_kid_10_feasible () Bool)
(declare-fun buttons_kid_9_x () Real)
(declare-fun buttons_kid_9_width () Real)
(declare-fun buttons_kid_9_feasible () Bool)
(declare-fun buttons_kid_8_width () Real)
(declare-fun buttons_kid_8_x () Real)
(declare-fun buttons_kid_8_feasible () Bool)
(declare-fun buttons_kid_7_width () Real)
(declare-fun buttons_kid_7_x () Real)
(declare-fun buttons_kid_7_feasible () Bool)
(declare-fun buttons_kid_6_width () Real)
(declare-fun buttons_kid_6_x () Real)
(declare-fun buttons_kid_6_feasible () Bool)
(declare-fun buttons_kid_5_width () Real)
(declare-fun buttons_kid_5_x () Real)
(declare-fun buttons_kid_5_feasible () Bool)
(declare-fun buttons_kid_4_x () Real)
(declare-fun buttons_kid_4_width () Real)
(declare-fun buttons_kid_4_feasible () Bool)
(declare-fun buttons_kid_3_x () Real)
(declare-fun buttons_kid_3_width () Real)
(declare-fun buttons_kid_3_feasible () Bool)
(declare-fun buttons_kid_2_x () Real)
(declare-fun buttons_kid_2_width () Real)
(declare-fun buttons_kid_2_feasible () Bool)
(declare-fun buttons_kid_1_width () Real)
(declare-fun buttons_kid_1_x () Real)
(declare-fun buttons_kid_1_feasible () Bool)
(declare-fun buttons_kid_0_width () Real)
(declare-fun buttons_kid_0_x () Real)
(declare-fun buttons_kid_0_feasible () Bool)
(declare-fun buttons_kid_16_y () Real)
(declare-fun buttons_y () Real)
(declare-fun buttons_kid_16_hight () Real)
(declare-fun buttons_hight () Real)
(declare-fun buttons_kid_15_y () Real)
(declare-fun buttons_kid_15_hight () Real)
(declare-fun buttons_kid_14_y () Real)
(declare-fun buttons_kid_14_hight () Real)
(declare-fun buttons_kid_13_y () Real)
(declare-fun buttons_kid_13_hight () Real)
(declare-fun buttons_kid_12_y () Real)
(declare-fun buttons_kid_12_hight () Real)
(declare-fun buttons_kid_11_y () Real)
(declare-fun buttons_kid_11_hight () Real)
(declare-fun buttons_kid_10_y () Real)
(declare-fun buttons_kid_10_hight () Real)
(declare-fun buttons_kid_9_y () Real)
(declare-fun buttons_kid_9_hight () Real)
(declare-fun buttons_kid_8_y () Real)
(declare-fun buttons_kid_8_hight () Real)
(declare-fun buttons_kid_7_y () Real)
(declare-fun buttons_kid_7_hight () Real)
(declare-fun buttons_kid_6_y () Real)
(declare-fun buttons_kid_6_hight () Real)
(declare-fun buttons_kid_5_y () Real)
(declare-fun buttons_kid_5_hight () Real)
(declare-fun buttons_kid_4_y () Real)
(declare-fun buttons_kid_4_hight () Real)
(declare-fun buttons_kid_3_y () Real)
(declare-fun buttons_kid_3_hight () Real)
(declare-fun buttons_kid_2_y () Real)
(declare-fun buttons_kid_2_hight () Real)
(declare-fun buttons_kid_1_y () Real)
(declare-fun buttons_kid_1_hight () Real)
(declare-fun buttons_kid_0_y () Real)
(declare-fun buttons_kid_0_hight () Real)
(declare-fun search_bar_kid_0_width () Real)
(declare-fun search_bar_kid_1_width () Real)
(declare-fun search_bar_y () Real)
(declare-fun search_bar_kid_1_hight () Real)
(declare-fun search_bar_hight () Real)
(declare-fun search_bar_kid_1_y () Real)
(declare-fun search_bar_kid_0_hight () Real)
(declare-fun search_bar_kid_0_y () Real)
(declare-fun search_bar_width () Real)
(declare-fun search_bar_kid_1_x () Real)
(declare-fun search_bar_x () Real)
(declare-fun search_bar_kid_0_x () Real)
(declare-fun search_kid_6_width () Real)
(declare-fun search_kid_5_width () Real)
(declare-fun search_kid_4_width () Real)
(declare-fun search_kid_3_width () Real)
(declare-fun search_kid_1_width () Real)
(declare-fun search_kid_0_width () Real)
(declare-fun search_hight () Real)
(declare-fun search_kid_6_x () Real)
(declare-fun search_kid_5_x () Real)
(declare-fun search_kid_4_x () Real)
(declare-fun search_kid_3_x () Real)
(declare-fun search_kid_1_x () Real)
(declare-fun search_kid_0_x () Real)
(declare-fun search_kid_6_hight () Real)
(declare-fun search_kid_6_y () Real)
(declare-fun search_y () Real)
(declare-fun search_x () Real)
(declare-fun search_width () Real)
(declare-fun search_kid_5_hight () Real)
(declare-fun search_kid_5_y () Real)
(declare-fun search_kid_4_hight () Real)
(declare-fun search_kid_4_y () Real)
(declare-fun search_kid_3_y () Real)
(declare-fun search_kid_3_hight () Real)
(declare-fun search_kid_1_hight () Real)
(declare-fun search_kid_1_y () Real)
(declare-fun search_kid_0_hight () Real)
(declare-fun search_kid_0_y () Real)
(declare-fun title_hight () Real)
(declare-fun title_y () Real)
(declare-fun title_width () Real)
(declare-fun title_x () Real)
(declare-fun BC_y () Real)
(declare-fun back_ground_y () Real)
(declare-fun back_ground_width () Real)
(declare-fun BC_x () Real)
(declare-fun back_ground_x () Real)
(declare-fun BC_width () Real)
(declare-fun back_ground_hight () Real)
(declare-fun BC_feasible () Bool)
(declare-fun BC_hight () Real)
(assert
 (let (($x1908 (not homes_feasible)))
 (let (($x2823 (or $x1908 homes_kid_3_feasible)))
 (let (($x2821 (not homes_kid_3_feasible)))
 (let (($x2822 (or $x2821 homes_feasible)))
 (let (($x2820 (or $x1908 homes_kid_2_feasible)))
 (let (($x2818 (not homes_kid_2_feasible)))
 (let (($x2819 (or $x2818 homes_feasible)))
 (let (($x2817 (or $x1908 homes_kid_1_feasible)))
 (let (($x2815 (not homes_kid_1_feasible)))
 (let (($x2816 (or $x2815 homes_feasible)))
 (let (($x2814 (or $x1908 homes_kid_0_feasible)))
 (let (($x2812 (not homes_kid_0_feasible)))
 (let (($x2813 (or $x2812 homes_feasible)))
 (let (($x1825 (not menus_feasible)))
 (let (($x2811 (or $x1825 menus_kid_1_feasible)))
 (let (($x2809 (not menus_kid_1_feasible)))
 (let (($x2810 (or $x2809 menus_feasible)))
 (let (($x2808 (or $x1825 menus_kid_0_feasible)))
 (let (($x2806 (not menus_kid_0_feasible)))
 (let (($x2807 (or $x2806 menus_feasible)))
 (let (($x1532 (not ads_top_2_feasible)))
 (let (($x2805 (or $x1532 homes_feasible)))
 (let (($x2804 (or $x1908 ads_top_2_feasible)))
 (let (($x2803 (or $x1532 menus_feasible)))
 (let (($x2802 (or $x1825 ads_top_2_feasible)))
 (let (($x1517 (not ads_top_1_feasible)))
 (let (($x2801 (or $x1517 ads_top_1_kid_4_feasible)))
 (let (($x2799 (not ads_top_1_kid_4_feasible)))
 (let (($x2800 (or $x2799 ads_top_1_feasible)))
 (let (($x2798 (or $x1517 categories_feasible)))
 (let (($x2796 (not categories_feasible)))
 (let (($x2797 (or $x2796 ads_top_1_feasible)))
 (let (($x2795 (or $x1517 store_feasible)))
 (let (($x2793 (not store_feasible)))
 (let (($x2794 (or $x2793 ads_top_1_feasible)))
 (let (($x2792 (or $x1517 home_feasible)))
 (let (($x2790 (not home_feasible)))
 (let (($x2791 (or $x2790 ads_top_1_feasible)))
 (let (($x2789 (or $x1517 prime_top_feasible)))
 (let (($x2787 (not prime_top_feasible)))
 (let (($x2788 (or $x2787 ads_top_1_feasible)))
 (let (($x1283 (not ads_pics_feasible)))
 (let (($x2786 (or $x1283 left_buttons_detail_feasible)))
 (let (($x2784 (not left_buttons_detail_feasible)))
 (let (($x2785 (or $x2784 ads_pics_feasible)))
 (let (($x2781 (not left_buttons_watch_feasible)))
 (let (($x1299 (not ads_pics_2_feasible)))
 (let (($x2783 (or $x1283 $x1299 $x2781)))
 (let (($x2782 (or ads_pics_feasible ads_pics_2_feasible $x2781)))
 (let (($x2780 (or $x1299 left_buttons_watch_feasible)))
 (let (($x2779 (or $x1283 left_buttons_watch_feasible)))
 (let (($x2776 (not left_buttons_title_feasible)))
 (let (($x2778 (or $x1283 $x1299 $x2776)))
 (let (($x2777 (or ads_pics_feasible ads_pics_2_feasible $x2776)))
 (let (($x2775 (or $x1299 left_buttons_title_feasible)))
 (let (($x2774 (or $x1283 left_buttons_title_feasible)))
 (let (($x2773 (= back_to_top_width 200.0)))
 (let ((?x2770 (* 2.0 back_to_top_x)))
 (let (($x2772 (= (+ (- (+ (* (- 2.0) info_x) back_to_top_width) info_width) ?x2770) 0.0)))
 (let (($x2766 (= info_hight 50.0)))
 (let (($x2765 (= (- (+ (- back_to_top_y info_y) back_to_top_hight) info_hight) 0.0)))
 (let ((?x2755 (- back_to_top_y info_y)))
 (let (($x2762 (= ?x2755 0.0)))
 (let ((?x2760 (+ (- (+ (- back_to_top_y) info_y) back_to_top_hight) info_hight)))
 (let (($x2761 (>= ?x2760 0.0)))
 (let (($x2756 (>= ?x2755 0.0)))
 (let (($x2754 (>= (- (+ (- info_x back_to_top_width) info_width) back_to_top_x) 0.0)))
 (let (($x2750 (>= (+ (- info_x) back_to_top_x) 0.0)))
 (let (($x2748 (>= back_to_top_hight 0.0)))
 (let (($x2747 (>= back_to_top_width 0.0)))
 (let (($x2746 (>= back_to_top_y 0.0)))
 (let (($x2745 (>= back_to_top_x 0.0)))
 (let ((?x2739 (+ (- (+ (- video_3_body_x) video_3_body_kid_6_x) video_3_body_width) video_3_body_kid_6_width)))
 (let (($x2740 (<= ?x2739 0.0)))
 (let (($x2743 (not video_3_body_kid_6_feasible)))
 (let (($x2744 (or $x2743 $x2740)))
 (let (($x2742 (or (not $x2740) video_3_body_kid_6_feasible)))
 (let ((?x2731 (+ (+ (- (- video_3_body_x) video_3_body_width) video_3_body_kid_5_x) video_3_body_kid_5_width)))
 (let (($x2732 (<= ?x2731 0.0)))
 (let (($x2735 (not video_3_body_kid_5_feasible)))
 (let (($x2736 (or $x2735 $x2732)))
 (let (($x2734 (or (not $x2732) video_3_body_kid_5_feasible)))
 (let ((?x2724 (+ (- (+ (- video_3_body_x) video_3_body_kid_4_x) video_3_body_width) video_3_body_kid_4_width)))
 (let (($x2725 (<= ?x2724 0.0)))
 (let (($x2728 (not video_3_body_kid_4_feasible)))
 (let (($x2729 (or $x2728 $x2725)))
 (let (($x2727 (or (not $x2725) video_3_body_kid_4_feasible)))
 (let ((?x2716 (+ (+ (- (- video_3_body_x) video_3_body_width) video_3_body_kid_3_x) video_3_body_kid_3_width)))
 (let (($x2717 (<= ?x2716 0.0)))
 (let (($x2720 (not video_3_body_kid_3_feasible)))
 (let (($x2721 (or $x2720 $x2717)))
 (let (($x2719 (or (not $x2717) video_3_body_kid_3_feasible)))
 (let ((?x2709 (+ (+ (- (- video_3_body_x) video_3_body_width) video_3_body_kid_2_x) video_3_body_kid_2_width)))
 (let (($x2710 (<= ?x2709 0.0)))
 (let (($x2713 (not video_3_body_kid_2_feasible)))
 (let (($x2714 (or $x2713 $x2710)))
 (let (($x2712 (or (not $x2710) video_3_body_kid_2_feasible)))
 (let ((?x2700 (- (+ (- video_3_body_x) video_3_body_kid_1_width) video_3_body_width)))
 (let (($x2702 (<= (+ ?x2700 video_3_body_kid_1_x) 0.0)))
 (let (($x2705 (not video_3_body_kid_1_feasible)))
 (let (($x2706 (or $x2705 $x2702)))
 (let (($x2704 (or (not $x2702) video_3_body_kid_1_feasible)))
 (let ((?x2692 (- (+ (- video_3_body_x) video_3_body_kid_0_width) video_3_body_width)))
 (let (($x2694 (<= (+ ?x2692 video_3_body_kid_0_x) 0.0)))
 (let (($x2697 (not video_3_body_kid_0_feasible)))
 (let (($x2698 (or $x2697 $x2694)))
 (let (($x2696 (or (not $x2694) video_3_body_kid_0_feasible)))
 (let ((?x2689 (- (- (+ (- 10.0) video_3_body_kid_6_x) video_3_body_kid_5_x) video_3_body_kid_5_width)))
 (let (($x2690 (= ?x2689 0.0)))
 (let ((?x2685 (- (+ (- (- 10.0) video_3_body_kid_4_x) video_3_body_kid_5_x) video_3_body_kid_4_width)))
 (let (($x2686 (= ?x2685 0.0)))
 (let ((?x2681 (- (- (+ (- 10.0) video_3_body_kid_4_x) video_3_body_kid_3_x) video_3_body_kid_3_width)))
 (let (($x2682 (= ?x2681 0.0)))
 (let ((?x2677 (- (- (+ (- 10.0) video_3_body_kid_3_x) video_3_body_kid_2_x) video_3_body_kid_2_width)))
 (let (($x2678 (= ?x2677 0.0)))
 (let ((?x2673 (+ (- (- (- 10.0) video_3_body_kid_1_width) video_3_body_kid_1_x) video_3_body_kid_2_x)))
 (let (($x2674 (= ?x2673 0.0)))
 (let ((?x2669 (- (+ (- (- 10.0) video_3_body_kid_0_width) video_3_body_kid_1_x) video_3_body_kid_0_x)))
 (let (($x2670 (= ?x2669 0.0)))
 (let ((?x2653 (- video_3_body_y)))
 (let ((?x2662 (+ ?x2653 video_3_body_kid_6_y)))
 (let (($x2666 (= ?x2662 0.0)))
 (let (($x2665 (= (+ (- ?x2662 video_3_body_hight) video_3_body_kid_6_hight) 0.0)))
 (let (($x2661 (= (+ ?x2653 video_3_body_kid_5_y) 0.0)))
 (let ((?x2658 (+ (- (- video_3_body_kid_5_hight video_3_body_y) video_3_body_hight) video_3_body_kid_5_y)))
 (let (($x2659 (= ?x2658 0.0)))
 (let (($x2655 (= (+ ?x2653 video_3_body_kid_4_y) 0.0)))
 (let ((?x2651 (- (+ (- video_3_body_kid_4_hight video_3_body_y) video_3_body_kid_4_y) video_3_body_hight)))
 (let (($x2652 (= ?x2651 0.0)))
 (let (($x2648 (= (- video_3_body_kid_3_y video_3_body_y) 0.0)))
 (let ((?x2645 (- (- (+ video_3_body_kid_3_y video_3_body_kid_3_hight) video_3_body_y) video_3_body_hight)))
 (let (($x2646 (= ?x2645 0.0)))
 (let (($x2642 (= (- video_3_body_kid_2_y video_3_body_y) 0.0)))
 (let ((?x2639 (- (- (+ video_3_body_kid_2_y video_3_body_kid_2_hight) video_3_body_y) video_3_body_hight)))
 (let (($x2640 (= ?x2639 0.0)))
 (let ((?x2632 (- video_3_body_kid_1_y video_3_body_y)))
 (let (($x2636 (= ?x2632 0.0)))
 (let (($x2635 (= (- (+ ?x2632 video_3_body_kid_1_hight) video_3_body_hight) 0.0)))
 (let ((?x2630 (- (+ (- video_3_body_kid_0_y video_3_body_y) video_3_body_kid_0_hight) video_3_body_hight)))
 (let (($x2631 (= ?x2630 0.0)))
 (let ((?x2627 (- video_3_body_kid_0_y video_3_body_y)))
 (let (($x2628 (= ?x2627 0.0)))
 (let (($x2626 (= (+ (- video_3_body_x) video_3_body_kid_0_x) 0.0)))
 (let ((?x2622 (+ (- (+ (- video_3_x) video_3_body_x) video_3_width) video_3_body_width)))
 (let (($x2623 (= ?x2622 0.0)))
 (let (($x2620 (= video_3_body_kid_6_width 250.0)))
 (let (($x2619 (= video_3_body_kid_5_width 250.0)))
 (let (($x2618 (= video_3_body_kid_4_width 250.0)))
 (let (($x2617 (= video_3_body_kid_3_width 250.0)))
 (let (($x2616 (= video_3_body_kid_2_width 250.0)))
 (let (($x2615 (= video_3_body_kid_1_width 250.0)))
 (let (($x2614 (= video_3_body_kid_0_width 250.0)))
 (let (($x2613 (>= video_3_body_kid_6_hight 0.0)))
 (let (($x2612 (>= video_3_body_kid_6_width 0.0)))
 (let (($x2611 (>= video_3_body_kid_6_y 0.0)))
 (let (($x2610 (>= video_3_body_kid_6_x 0.0)))
 (let (($x2609 (>= video_3_body_kid_5_hight 0.0)))
 (let (($x2608 (>= video_3_body_kid_5_width 0.0)))
 (let (($x2607 (>= video_3_body_kid_5_y 0.0)))
 (let (($x2606 (>= video_3_body_kid_5_x 0.0)))
 (let (($x2605 (>= video_3_body_kid_4_hight 0.0)))
 (let (($x2604 (>= video_3_body_kid_4_width 0.0)))
 (let (($x2603 (>= video_3_body_kid_4_y 0.0)))
 (let (($x2602 (>= video_3_body_kid_4_x 0.0)))
 (let (($x2601 (>= video_3_body_kid_3_hight 0.0)))
 (let (($x2600 (>= video_3_body_kid_3_width 0.0)))
 (let (($x2599 (>= video_3_body_kid_3_y 0.0)))
 (let (($x2598 (>= video_3_body_kid_3_x 0.0)))
 (let (($x2597 (>= video_3_body_kid_2_hight 0.0)))
 (let (($x2596 (>= video_3_body_kid_2_width 0.0)))
 (let (($x2595 (>= video_3_body_kid_2_y 0.0)))
 (let (($x2594 (>= video_3_body_kid_2_x 0.0)))
 (let (($x2593 (>= video_3_body_kid_1_hight 0.0)))
 (let (($x2592 (>= video_3_body_kid_1_width 0.0)))
 (let (($x2591 (>= video_3_body_kid_1_y 0.0)))
 (let (($x2590 (>= video_3_body_kid_1_x 0.0)))
 (let (($x2589 (>= video_3_body_kid_0_hight 0.0)))
 (let (($x2588 (>= video_3_body_kid_0_width 0.0)))
 (let (($x2587 (>= video_3_body_kid_0_y 0.0)))
 (let (($x2586 (>= video_3_body_kid_0_x 0.0)))
 (let (($x2585 (= (+ (- 50.0) video_3_title_hight) 0.0)))
 (let (($x2583 (= (+ (- 400.0) video_3_title_width) 0.0)))
 (let ((?x2580 (+ (- (+ (- video_3_y) video_3_body_y) video_3_hight) video_3_body_hight)))
 (let (($x2581 (= ?x2580 0.0)))
 (let ((?x2556 (- video_3_y)))
 (let ((?x2557 (+ ?x2556 video_3_title_y)))
 (let (($x2578 (= ?x2557 0.0)))
 (let ((?x2097 (- video_3_x)))
 (let ((?x2563 (+ ?x2097 video_3_body_x)))
 (let (($x2577 (= ?x2563 0.0)))
 (let ((?x2551 (+ ?x2097 video_3_title_x)))
 (let (($x2576 (= ?x2551 0.0)))
 (let ((?x2549 (- (+ (- video_3_title_hight) video_3_body_y) video_3_title_y)))
 (let (($x2575 (>= ?x2549 0.0)))
 (let ((?x2573 (- (+ (- video_3_y video_3_body_y) video_3_hight) video_3_body_hight)))
 (let (($x2574 (>= ?x2573 0.0)))
 (let ((?x2569 (+ ?x2556 video_3_body_y)))
 (let (($x2570 (>= ?x2569 0.0)))
 (let ((?x2567 (- (+ (- video_3_x video_3_body_x) video_3_width) video_3_body_width)))
 (let (($x2568 (>= ?x2567 0.0)))
 (let (($x2564 (>= ?x2563 0.0)))
 (let ((?x2561 (- (+ (+ (- video_3_title_hight) video_3_y) video_3_hight) video_3_title_y)))
 (let (($x2562 (>= ?x2561 0.0)))
 (let (($x2558 (>= ?x2557 0.0)))
 (let ((?x2554 (- (- (+ video_3_x video_3_width) video_3_title_x) video_3_title_width)))
 (let (($x2555 (>= ?x2554 0.0)))
 (let (($x2552 (>= ?x2551 0.0)))
 (let (($x2550 (= ?x2549 10.0)))
 (let (($x2546 (>= video_3_body_hight 0.0)))
 (let (($x2545 (>= video_3_body_width 0.0)))
 (let (($x2544 (>= video_3_body_y 0.0)))
 (let (($x2543 (>= video_3_body_x 0.0)))
 (let (($x2542 (>= video_3_title_hight 0.0)))
 (let (($x2541 (>= video_3_title_width 0.0)))
 (let (($x2540 (>= video_3_title_y 0.0)))
 (let (($x2539 (>= video_3_title_x 0.0)))
 (let ((?x2533 (+ (- (+ (- video_2_body_x) video_2_body_kid_6_x) video_2_body_width) video_2_body_kid_6_width)))
 (let (($x2534 (<= ?x2533 0.0)))
 (let (($x2537 (not video_2_body_kid_6_feasible)))
 (let (($x2538 (or $x2537 $x2534)))
 (let (($x2536 (or (not $x2534) video_2_body_kid_6_feasible)))
 (let ((?x2525 (+ (+ (- (- video_2_body_x) video_2_body_width) video_2_body_kid_5_x) video_2_body_kid_5_width)))
 (let (($x2526 (<= ?x2525 0.0)))
 (let (($x2529 (not video_2_body_kid_5_feasible)))
 (let (($x2530 (or $x2529 $x2526)))
 (let (($x2528 (or (not $x2526) video_2_body_kid_5_feasible)))
 (let ((?x2518 (+ (+ (- (- video_2_body_x) video_2_body_width) video_2_body_kid_4_x) video_2_body_kid_4_width)))
 (let (($x2519 (<= ?x2518 0.0)))
 (let (($x2522 (not video_2_body_kid_4_feasible)))
 (let (($x2523 (or $x2522 $x2519)))
 (let (($x2521 (or (not $x2519) video_2_body_kid_4_feasible)))
 (let ((?x2510 (+ (- (- video_2_body_kid_3_width video_2_body_x) video_2_body_width) video_2_body_kid_3_x)))
 (let (($x2511 (<= ?x2510 0.0)))
 (let (($x2514 (not video_2_body_kid_3_feasible)))
 (let (($x2515 (or $x2514 $x2511)))
 (let (($x2513 (or (not $x2511) video_2_body_kid_3_feasible)))
 (let ((?x2502 (+ (- (- video_2_body_kid_2_width video_2_body_x) video_2_body_width) video_2_body_kid_2_x)))
 (let (($x2503 (<= ?x2502 0.0)))
 (let (($x2506 (not video_2_body_kid_2_feasible)))
 (let (($x2507 (or $x2506 $x2503)))
 (let (($x2505 (or (not $x2503) video_2_body_kid_2_feasible)))
 (let ((?x2494 (- (+ (- video_2_body_kid_1_x video_2_body_x) video_2_body_kid_1_width) video_2_body_width)))
 (let (($x2495 (<= ?x2494 0.0)))
 (let (($x2498 (not video_2_body_kid_1_feasible)))
 (let (($x2499 (or $x2498 $x2495)))
 (let (($x2497 (or (not $x2495) video_2_body_kid_1_feasible)))
 (let ((?x2486 (+ (- (+ (- video_2_body_x) video_2_body_kid_0_x) video_2_body_width) video_2_body_kid_0_width)))
 (let (($x2487 (<= ?x2486 0.0)))
 (let (($x2490 (not video_2_body_kid_0_feasible)))
 (let (($x2491 (or $x2490 $x2487)))
 (let (($x2489 (or (not $x2487) video_2_body_kid_0_feasible)))
 (let ((?x2483 (- (- (+ (- 10.0) video_2_body_kid_6_x) video_2_body_kid_5_x) video_2_body_kid_5_width)))
 (let (($x2484 (= ?x2483 0.0)))
 (let ((?x2479 (- (- (+ (- 10.0) video_2_body_kid_5_x) video_2_body_kid_4_x) video_2_body_kid_4_width)))
 (let (($x2480 (= ?x2479 0.0)))
 (let ((?x2475 (+ (- (- (- 10.0) video_2_body_kid_3_width) video_2_body_kid_3_x) video_2_body_kid_4_x)))
 (let (($x2476 (= ?x2475 0.0)))
 (let ((?x2471 (- (+ (- (- 10.0) video_2_body_kid_2_width) video_2_body_kid_3_x) video_2_body_kid_2_x)))
 (let (($x2472 (= ?x2471 0.0)))
 (let ((?x2467 (+ (- (- (- 10.0) video_2_body_kid_1_x) video_2_body_kid_1_width) video_2_body_kid_2_x)))
 (let (($x2468 (= ?x2467 0.0)))
 (let ((?x2463 (- (- (+ (- 10.0) video_2_body_kid_1_x) video_2_body_kid_0_x) video_2_body_kid_0_width)))
 (let (($x2464 (= ?x2463 0.0)))
 (let (($x2460 (= (+ (- video_2_body_y) video_2_body_kid_6_y) 0.0)))
 (let ((?x2455 (- (+ (- video_2_body_hight) video_2_body_kid_6_hight) video_2_body_y)))
 (let (($x2457 (= (+ ?x2455 video_2_body_kid_6_y) 0.0)))
 (let (($x2453 (= (- video_2_body_kid_5_y video_2_body_y) 0.0)))
 (let ((?x2449 (+ (+ (- video_2_body_hight) video_2_body_kid_5_y) video_2_body_kid_5_hight)))
 (let (($x2451 (= (- ?x2449 video_2_body_y) 0.0)))
 (let (($x2447 (= (- video_2_body_kid_4_y video_2_body_y) 0.0)))
 (let ((?x2443 (+ (+ (- video_2_body_hight) video_2_body_kid_4_y) video_2_body_kid_4_hight)))
 (let (($x2445 (= (- ?x2443 video_2_body_y) 0.0)))
 (let (($x2441 (= (- video_2_body_kid_3_y video_2_body_y) 0.0)))
 (let ((?x2437 (+ (+ (- video_2_body_hight) video_2_body_kid_3_y) video_2_body_kid_3_hight)))
 (let (($x2439 (= (- ?x2437 video_2_body_y) 0.0)))
 (let (($x2435 (= (- video_2_body_kid_2_y video_2_body_y) 0.0)))
 (let ((?x2431 (+ (+ (- video_2_body_hight) video_2_body_kid_2_y) video_2_body_kid_2_hight)))
 (let (($x2433 (= (- ?x2431 video_2_body_y) 0.0)))
 (let (($x2428 (= (- video_2_body_kid_1_y video_2_body_y) 0.0)))
 (let ((?x2424 (+ (- video_2_body_kid_1_hight video_2_body_hight) video_2_body_kid_1_y)))
 (let (($x2426 (= (- ?x2424 video_2_body_y) 0.0)))
 (let ((?x2420 (+ (- video_2_body_kid_0_y video_2_body_hight) video_2_body_kid_0_hight)))
 (let (($x2422 (= (- ?x2420 video_2_body_y) 0.0)))
 (let (($x2418 (= (- video_2_body_kid_0_y video_2_body_y) 0.0)))
 (let ((?x2414 (- video_2_body_x)))
 (let ((?x2415 (+ ?x2414 video_2_body_kid_0_x)))
 (let (($x2416 (= ?x2415 0.0)))
 (let ((?x2412 (+ (- (+ (- video_2_x) video_2_body_x) video_2_width) video_2_body_width)))
 (let (($x2413 (= ?x2412 0.0)))
 (let (($x2410 (= video_2_body_kid_6_width 250.0)))
 (let (($x2409 (= video_2_body_kid_5_width 250.0)))
 (let (($x2408 (= video_2_body_kid_4_width 250.0)))
 (let (($x2407 (= video_2_body_kid_3_width 250.0)))
 (let (($x2406 (= video_2_body_kid_2_width 250.0)))
 (let (($x2405 (= video_2_body_kid_1_width 250.0)))
 (let (($x2404 (= video_2_body_kid_0_width 250.0)))
 (let (($x2403 (>= video_2_body_kid_6_hight 0.0)))
 (let (($x2402 (>= video_2_body_kid_6_width 0.0)))
 (let (($x2401 (>= video_2_body_kid_6_y 0.0)))
 (let (($x2400 (>= video_2_body_kid_6_x 0.0)))
 (let (($x2399 (>= video_2_body_kid_5_hight 0.0)))
 (let (($x2398 (>= video_2_body_kid_5_width 0.0)))
 (let (($x2397 (>= video_2_body_kid_5_y 0.0)))
 (let (($x2396 (>= video_2_body_kid_5_x 0.0)))
 (let (($x2395 (>= video_2_body_kid_4_hight 0.0)))
 (let (($x2394 (>= video_2_body_kid_4_width 0.0)))
 (let (($x2393 (>= video_2_body_kid_4_y 0.0)))
 (let (($x2392 (>= video_2_body_kid_4_x 0.0)))
 (let (($x2391 (>= video_2_body_kid_3_hight 0.0)))
 (let (($x2390 (>= video_2_body_kid_3_width 0.0)))
 (let (($x2389 (>= video_2_body_kid_3_y 0.0)))
 (let (($x2388 (>= video_2_body_kid_3_x 0.0)))
 (let (($x2387 (>= video_2_body_kid_2_hight 0.0)))
 (let (($x2386 (>= video_2_body_kid_2_width 0.0)))
 (let (($x2385 (>= video_2_body_kid_2_y 0.0)))
 (let (($x2384 (>= video_2_body_kid_2_x 0.0)))
 (let (($x2383 (>= video_2_body_kid_1_hight 0.0)))
 (let (($x2382 (>= video_2_body_kid_1_width 0.0)))
 (let (($x2381 (>= video_2_body_kid_1_y 0.0)))
 (let (($x2380 (>= video_2_body_kid_1_x 0.0)))
 (let (($x2379 (>= video_2_body_kid_0_hight 0.0)))
 (let (($x2378 (>= video_2_body_kid_0_width 0.0)))
 (let (($x2377 (>= video_2_body_kid_0_y 0.0)))
 (let (($x2376 (>= video_2_body_kid_0_x 0.0)))
 (let (($x2375 (= (+ (- 50.0) video_2_title_hight) 0.0)))
 (let (($x2373 (= (+ (- 400.0) video_2_title_width) 0.0)))
 (let ((?x2370 (+ (- (+ (- video_2_hight) video_2_body_hight) video_2_y) video_2_body_y)))
 (let (($x2371 (= ?x2370 0.0)))
 (let ((?x2345 (- video_2_title_y video_2_y)))
 (let (($x2367 (= ?x2345 0.0)))
 (let ((?x2085 (- video_2_x)))
 (let ((?x2351 (+ ?x2085 video_2_body_x)))
 (let (($x2366 (= ?x2351 0.0)))
 (let ((?x2339 (+ ?x2085 video_2_title_x)))
 (let (($x2365 (= ?x2339 0.0)))
 (let ((?x2337 (+ (- (- video_2_title_y) video_2_title_hight) video_2_body_y)))
 (let (($x2364 (>= ?x2337 0.0)))
 (let ((?x2362 (- (+ (- video_2_hight video_2_body_hight) video_2_y) video_2_body_y)))
 (let (($x2363 (>= ?x2362 0.0)))
 (let (($x2359 (>= (+ (- video_2_y) video_2_body_y) 0.0)))
 (let ((?x2355 (- (+ (- video_2_x video_2_body_x) video_2_width) video_2_body_width)))
 (let (($x2356 (>= ?x2355 0.0)))
 (let (($x2352 (>= ?x2351 0.0)))
 (let ((?x2349 (+ (- (- video_2_hight video_2_title_y) video_2_title_hight) video_2_y)))
 (let (($x2350 (>= ?x2349 0.0)))
 (let (($x2346 (>= ?x2345 0.0)))
 (let ((?x2343 (- (- (+ video_2_x video_2_width) video_2_title_x) video_2_title_width)))
 (let (($x2344 (>= ?x2343 0.0)))
 (let (($x2340 (>= ?x2339 0.0)))
 (let (($x2338 (= ?x2337 10.0)))
 (let (($x2334 (>= video_2_body_hight 0.0)))
 (let (($x2333 (>= video_2_body_width 0.0)))
 (let (($x2332 (>= video_2_body_y 0.0)))
 (let (($x2331 (>= video_2_body_x 0.0)))
 (let (($x2330 (>= video_2_title_hight 0.0)))
 (let (($x2329 (>= video_2_title_width 0.0)))
 (let (($x2328 (>= video_2_title_y 0.0)))
 (let (($x2327 (>= video_2_title_x 0.0)))
 (let ((?x2321 (+ (- (+ (- video_1_body_width) video_1_body_kid_6_x) video_1_body_x) video_1_body_kid_6_width)))
 (let (($x2322 (<= ?x2321 0.0)))
 (let (($x2325 (not video_1_body_kid_6_feasible)))
 (let (($x2326 (or $x2325 $x2322)))
 (let (($x2324 (or (not $x2322) video_1_body_kid_6_feasible)))
 (let ((?x2312 (+ (+ (- video_1_body_width) video_1_body_kid_5_width) video_1_body_kid_5_x)))
 (let (($x2314 (<= (- ?x2312 video_1_body_x) 0.0)))
 (let (($x2317 (not video_1_body_kid_5_feasible)))
 (let (($x2318 (or $x2317 $x2314)))
 (let (($x2316 (or (not $x2314) video_1_body_kid_5_feasible)))
 (let ((?x2304 (- (+ (- video_1_body_width) video_1_body_kid_4_width) video_1_body_x)))
 (let (($x2306 (<= (+ ?x2304 video_1_body_kid_4_x) 0.0)))
 (let (($x2309 (not video_1_body_kid_4_feasible)))
 (let (($x2310 (or $x2309 $x2306)))
 (let (($x2308 (or (not $x2306) video_1_body_kid_4_feasible)))
 (let ((?x2296 (+ (+ (- video_1_body_width) video_1_body_kid_3_x) video_1_body_kid_3_width)))
 (let (($x2298 (<= (- ?x2296 video_1_body_x) 0.0)))
 (let (($x2301 (not video_1_body_kid_3_feasible)))
 (let (($x2302 (or $x2301 $x2298)))
 (let (($x2300 (or (not $x2298) video_1_body_kid_3_feasible)))
 (let ((?x2288 (+ (+ (- video_1_body_width) video_1_body_kid_2_x) video_1_body_kid_2_width)))
 (let (($x2290 (<= (- ?x2288 video_1_body_x) 0.0)))
 (let (($x2293 (not video_1_body_kid_2_feasible)))
 (let (($x2294 (or $x2293 $x2290)))
 (let (($x2292 (or (not $x2290) video_1_body_kid_2_feasible)))
 (let ((?x2280 (+ (+ (- video_1_body_width) video_1_body_kid_1_x) video_1_body_kid_1_width)))
 (let (($x2282 (<= (- ?x2280 video_1_body_x) 0.0)))
 (let (($x2285 (not video_1_body_kid_1_feasible)))
 (let (($x2286 (or $x2285 $x2282)))
 (let (($x2284 (or (not $x2282) video_1_body_kid_1_feasible)))
 (let ((?x2273 (+ (- (+ (- video_1_body_width) video_1_body_kid_0_x) video_1_body_x) video_1_body_kid_0_width)))
 (let (($x2274 (<= ?x2273 0.0)))
 (let (($x2277 (not video_1_body_kid_0_feasible)))
 (let (($x2278 (or $x2277 $x2274)))
 (let (($x2276 (or (not $x2274) video_1_body_kid_0_feasible)))
 (let ((?x2269 (+ (- (- (- 10.0) video_1_body_kid_5_width) video_1_body_kid_5_x) video_1_body_kid_6_x)))
 (let (($x2270 (= ?x2269 0.0)))
 (let ((?x2265 (- (+ (- (- 10.0) video_1_body_kid_4_width) video_1_body_kid_5_x) video_1_body_kid_4_x)))
 (let (($x2266 (= ?x2265 0.0)))
 (let ((?x2261 (+ (- (- (- 10.0) video_1_body_kid_3_x) video_1_body_kid_3_width) video_1_body_kid_4_x)))
 (let (($x2262 (= ?x2261 0.0)))
 (let ((?x2257 (- (- (+ (- 10.0) video_1_body_kid_3_x) video_1_body_kid_2_x) video_1_body_kid_2_width)))
 (let (($x2258 (= ?x2257 0.0)))
 (let ((?x2253 (- (+ (- (- 10.0) video_1_body_kid_1_x) video_1_body_kid_2_x) video_1_body_kid_1_width)))
 (let (($x2254 (= ?x2253 0.0)))
 (let ((?x2249 (- (- (+ (- 10.0) video_1_body_kid_1_x) video_1_body_kid_0_x) video_1_body_kid_0_width)))
 (let (($x2250 (= ?x2249 0.0)))
 (let ((?x2242 (- video_1_body_kid_6_y video_1_body_y)))
 (let (($x2246 (= ?x2242 0.0)))
 (let (($x2245 (= (- (+ ?x2242 video_1_body_kid_6_hight) video_1_body_hight) 0.0)))
 (let ((?x2213 (- video_1_body_y)))
 (let ((?x2237 (+ ?x2213 video_1_body_kid_5_y)))
 (let (($x2241 (= ?x2237 0.0)))
 (let (($x2240 (= (+ (- ?x2237 video_1_body_hight) video_1_body_kid_5_hight) 0.0)))
 (let ((?x2232 (+ ?x2213 video_1_body_kid_4_y)))
 (let (($x2236 (= ?x2232 0.0)))
 (let (($x2235 (= (+ (- ?x2232 video_1_body_hight) video_1_body_kid_4_hight) 0.0)))
 (let (($x2231 (= (+ ?x2213 video_1_body_kid_3_y) 0.0)))
 (let ((?x2228 (+ (+ (- ?x2213 video_1_body_hight) video_1_body_kid_3_y) video_1_body_kid_3_hight)))
 (let (($x2229 (= ?x2228 0.0)))
 (let (($x2225 (= (+ ?x2213 video_1_body_kid_2_y) 0.0)))
 (let ((?x2222 (+ (- (- video_1_body_kid_2_hight video_1_body_y) video_1_body_hight) video_1_body_kid_2_y)))
 (let (($x2223 (= ?x2222 0.0)))
 (let (($x2219 (= (+ ?x2213 video_1_body_kid_1_y) 0.0)))
 (let ((?x2216 (+ (- (+ ?x2213 video_1_body_kid_1_hight) video_1_body_hight) video_1_body_kid_1_y)))
 (let (($x2217 (= ?x2216 0.0)))
 (let ((?x2211 (- (+ (- video_1_body_kid_0_y video_1_body_y) video_1_body_kid_0_hight) video_1_body_hight)))
 (let (($x2212 (= ?x2211 0.0)))
 (let ((?x2208 (- video_1_body_kid_0_y video_1_body_y)))
 (let (($x2209 (= ?x2208 0.0)))
 (let (($x2207 (= (- video_1_body_kid_0_x video_1_body_x) 0.0)))
 (let ((?x2204 (+ (- (- video_1_body_width video_1_x) video_1_width) video_1_body_x)))
 (let (($x2205 (= ?x2204 0.0)))
 (let (($x2201 (= video_1_body_kid_6_width 250.0)))
 (let (($x2200 (= video_1_body_kid_5_width 250.0)))
 (let (($x2199 (= video_1_body_kid_4_width 250.0)))
 (let (($x2198 (= video_1_body_kid_3_width 250.0)))
 (let (($x2197 (= video_1_body_kid_2_width 250.0)))
 (let (($x2196 (= video_1_body_kid_1_width 250.0)))
 (let (($x2195 (= video_1_body_kid_0_width 250.0)))
 (let (($x2193 (>= video_1_body_kid_6_hight 0.0)))
 (let (($x2192 (>= video_1_body_kid_6_width 0.0)))
 (let (($x2191 (>= video_1_body_kid_6_y 0.0)))
 (let (($x2190 (>= video_1_body_kid_6_x 0.0)))
 (let (($x2189 (>= video_1_body_kid_5_hight 0.0)))
 (let (($x2188 (>= video_1_body_kid_5_width 0.0)))
 (let (($x2187 (>= video_1_body_kid_5_y 0.0)))
 (let (($x2186 (>= video_1_body_kid_5_x 0.0)))
 (let (($x2185 (>= video_1_body_kid_4_hight 0.0)))
 (let (($x2184 (>= video_1_body_kid_4_width 0.0)))
 (let (($x2183 (>= video_1_body_kid_4_y 0.0)))
 (let (($x2182 (>= video_1_body_kid_4_x 0.0)))
 (let (($x2181 (>= video_1_body_kid_3_hight 0.0)))
 (let (($x2180 (>= video_1_body_kid_3_width 0.0)))
 (let (($x2179 (>= video_1_body_kid_3_y 0.0)))
 (let (($x2178 (>= video_1_body_kid_3_x 0.0)))
 (let (($x2177 (>= video_1_body_kid_2_hight 0.0)))
 (let (($x2176 (>= video_1_body_kid_2_width 0.0)))
 (let (($x2175 (>= video_1_body_kid_2_y 0.0)))
 (let (($x2174 (>= video_1_body_kid_2_x 0.0)))
 (let (($x2173 (>= video_1_body_kid_1_hight 0.0)))
 (let (($x2172 (>= video_1_body_kid_1_width 0.0)))
 (let (($x2171 (>= video_1_body_kid_1_y 0.0)))
 (let (($x2170 (>= video_1_body_kid_1_x 0.0)))
 (let (($x2169 (>= video_1_body_kid_0_hight 0.0)))
 (let (($x2168 (>= video_1_body_kid_0_width 0.0)))
 (let (($x2167 (>= video_1_body_kid_0_y 0.0)))
 (let (($x2166 (>= video_1_body_kid_0_x 0.0)))
 (let (($x2165 (= (+ (- 50.0) video_1_title_hight) 0.0)))
 (let (($x2162 (= (+ (- 400.0) video_1_title_width) 0.0)))
 (let ((?x2158 (+ (+ (- (- video_1_y) video_1_hight) video_1_body_y) video_1_body_hight)))
 (let (($x2159 (= ?x2158 0.0)))
 (let ((?x2042 (- video_1_y)))
 (let ((?x2135 (+ ?x2042 video_1_title_y)))
 (let (($x2156 (= ?x2135 0.0)))
 (let ((?x2127 (- video_1_x)))
 (let ((?x2141 (+ ?x2127 video_1_body_x)))
 (let (($x2155 (= ?x2141 0.0)))
 (let ((?x2128 (+ ?x2127 video_1_title_x)))
 (let (($x2154 (= ?x2128 0.0)))
 (let ((?x2125 (- (- video_1_body_y video_1_title_y) video_1_title_hight)))
 (let (($x2153 (>= ?x2125 0.0)))
 (let ((?x2151 (- (- (+ video_1_y video_1_hight) video_1_body_y) video_1_body_hight)))
 (let (($x2152 (>= ?x2151 0.0)))
 (let (($x2149 (>= (+ ?x2042 video_1_body_y) 0.0)))
 (let ((?x2146 (- (+ (+ (- video_1_body_width) video_1_x) video_1_width) video_1_body_x)))
 (let (($x2147 (>= ?x2146 0.0)))
 (let (($x2142 (>= ?x2141 0.0)))
 (let ((?x2139 (- (- (+ video_1_y video_1_hight) video_1_title_y) video_1_title_hight)))
 (let (($x2140 (>= ?x2139 0.0)))
 (let (($x2136 (>= ?x2135 0.0)))
 (let ((?x2133 (- (+ (+ (- video_1_title_width) video_1_x) video_1_width) video_1_title_x)))
 (let (($x2134 (>= ?x2133 0.0)))
 (let (($x2129 (>= ?x2128 0.0)))
 (let (($x2126 (= ?x2125 10.0)))
 (let (($x2123 (>= video_1_body_hight 0.0)))
 (let (($x2122 (>= video_1_body_width 0.0)))
 (let (($x2121 (>= video_1_body_y 0.0)))
 (let (($x2120 (>= video_1_body_x 0.0)))
 (let (($x2119 (>= video_1_title_hight 0.0)))
 (let (($x2118 (>= video_1_title_width 0.0)))
 (let (($x2117 (>= video_1_title_y 0.0)))
 (let (($x2116 (>= video_1_title_x 0.0)))
 (let (($x2115 (= video_1_hight 200.0)))
 (let (($x2113 (= (- video_1_hight video_3_hight) 0.0)))
 (let (($x2111 (= (+ (- video_2_hight) video_1_hight) 0.0)))
 (let ((?x2049 (- (+ (- video_2_hight) video_3_y) video_2_y)))
 (let (($x2109 (>= ?x2049 0.0)))
 (let ((?x2043 (- ?x2042 video_1_hight)))
 (let ((?x2044 (+ ?x2043 video_2_y)))
 (let (($x2108 (>= ?x2044 0.0)))
 (let (($x2107 (>= (+ (- (- mainbody_hight video_3_y) video_3_hight) mainbody_y) 40.0)))
 (let (($x2103 (>= (- video_3_y mainbody_y) 40.0)))
 (let (($x2101 (>= (+ (+ (- ?x2097 video_3_width) mainbody_x) mainbody_width) 40.0)))
 (let ((?x2055 (- video_3_x mainbody_x)))
 (let (($x2096 (>= ?x2055 40.0)))
 (let ((?x2094 (+ (- (+ (- video_2_hight) mainbody_hight) video_2_y) mainbody_y)))
 (let (($x2095 (>= ?x2094 40.0)))
 (let (($x2091 (>= (- video_2_y mainbody_y) 40.0)))
 (let (($x2089 (>= (+ (- (+ ?x2085 mainbody_x) video_2_width) mainbody_width) 40.0)))
 (let ((?x2053 (- video_2_x mainbody_x)))
 (let (($x2084 (>= ?x2053 40.0)))
 (let (($x2083 (>= (+ (- (+ ?x2042 mainbody_hight) video_1_hight) mainbody_y) 40.0)))
 (let ((?x2068 (- video_1_y mainbody_y)))
 (let (($x2079 (>= ?x2068 40.0)))
 (let (($x2078 (>= (- (+ (- mainbody_x video_1_x) mainbody_width) video_1_width) 40.0)))
 (let ((?x504 (- mainbody_x)))
 (let ((?x2051 (+ ?x504 video_1_x)))
 (let (($x2074 (>= ?x2051 40.0)))
 (let ((?x2072 (- (+ (+ (- mainbody_hight) video_3_y) video_3_hight) mainbody_y)))
 (let (($x2073 (= ?x2072 (- 40.0))))
 (let (($x2069 (= ?x2068 40.0)))
 (let (($x2067 (= (- (- (+ video_3_x video_3_width) mainbody_x) mainbody_width) (- 40.0))))
 (let (($x2063 (= (- (+ ?x2053 video_2_width) mainbody_width) (- 40.0))))
 (let (($x2060 (= (+ (- ?x2051 mainbody_width) video_1_width) (- 40.0))))
 (let (($x2056 (= ?x2055 40.0)))
 (let (($x2054 (= ?x2053 40.0)))
 (let (($x2052 (= ?x2051 40.0)))
 (let (($x2050 (= ?x2049 20.0)))
 (let (($x2046 (= ?x2044 20.0)))
 (let (($x2041 (>= video_3_hight 0.0)))
 (let (($x2040 (>= video_3_width 0.0)))
 (let (($x2039 (>= video_3_y 0.0)))
 (let (($x2038 (>= video_3_x 0.0)))
 (let (($x2037 (>= video_2_hight 0.0)))
 (let (($x2036 (>= video_2_width 0.0)))
 (let (($x2035 (>= video_2_y 0.0)))
 (let (($x2034 (>= video_2_x 0.0)))
 (let (($x2033 (>= video_1_hight 0.0)))
 (let (($x2032 (>= video_1_width 0.0)))
 (let (($x2031 (>= video_1_y 0.0)))
 (let (($x2030 (>= video_1_x 0.0)))
 (let (($x2029 (or $x1908 (= (- (- homes_kid_3_x homes_kid_2_x) homes_kid_2_width) 10.0))))
 (let ((?x1979 (- (+ (- homes_kid_1_width) homes_kid_2_x) homes_kid_1_x)))
 (let (($x2027 (or $x1908 (= ?x1979 10.0))))
 (let ((?x1975 (- (+ (- homes_kid_0_width) homes_kid_1_x) homes_kid_0_x)))
 (let (($x2025 (or $x1908 (= ?x1975 10.0))))
 (let (($x2023 (or $x1908 (= (+ (- homes_x) homes_kid_0_x) 10.0))))
 (let ((?x2019 (+ (+ (- (- homes_y) homes_hight) homes_kid_3_hight) homes_kid_3_y)))
 (let (($x2021 (or $x1908 (= ?x2019 (- 10.0)))))
 (let (($x2017 (or $x1908 (= (+ (- homes_y) homes_kid_3_y) 10.0))))
 (let ((?x2013 (+ (- (+ (- homes_y) homes_kid_2_y) homes_hight) homes_kid_2_hight)))
 (let (($x2015 (or $x1908 (= ?x2013 (- 10.0)))))
 (let (($x2011 (or $x1908 (= (+ (- homes_y) homes_kid_2_y) 10.0))))
 (let ((?x2007 (+ (+ (- (- homes_y) homes_hight) homes_kid_1_y) homes_kid_1_hight)))
 (let (($x2009 (or $x1908 (= ?x2007 (- 10.0)))))
 (let (($x2005 (or $x1908 (= (+ (- homes_y) homes_kid_1_y) 10.0))))
 (let ((?x2001 (+ (+ (- (- homes_y) homes_hight) homes_kid_0_y) homes_kid_0_hight)))
 (let (($x2003 (or $x1908 (= ?x2001 (- 10.0)))))
 (let (($x1998 (or $x1908 (= (+ (- homes_y) homes_kid_0_y) 10.0))))
 (let (($x1996 (or $x1908 (= homes_kid_0_width 100.0))))
 (let (($x1994 (or $x1908 (= (- homes_kid_0_width homes_kid_3_width) 0.0))))
 (let (($x1991 (or $x1908 (= (- homes_kid_0_width homes_kid_2_width) 0.0))))
 (let (($x1988 (or $x1908 (= (+ (- homes_kid_1_width) homes_kid_0_width) 0.0))))
 (let (($x1985 (or $x1908 (>= (- (- homes_kid_3_x homes_kid_2_x) homes_kid_2_width) 0.0))))
 (let (($x1981 (or $x1908 (>= ?x1979 0.0))))
 (let (($x1977 (or $x1908 (>= ?x1975 0.0))))
 (let (($x1972 (>= (- (- (+ homes_y homes_hight) homes_kid_3_hight) homes_kid_3_y) 10.0)))
 (let (($x1973 (or $x1908 $x1972)))
 (let (($x1969 (or $x1908 (>= (+ (- homes_y) homes_kid_3_y) 10.0))))
 (let ((?x1964 (+ (- (+ (- homes_kid_3_x) homes_x) homes_kid_3_width) homes_width)))
 (let (($x1966 (or $x1908 (>= ?x1964 10.0))))
 (let (($x1960 (or $x1908 (>= (- homes_kid_3_x homes_x) 10.0))))
 (let (($x1956 (>= (- (+ (- homes_y homes_kid_2_y) homes_hight) homes_kid_2_hight) 10.0)))
 (let (($x1957 (or $x1908 $x1956)))
 (let (($x1952 (or $x1908 (>= (+ (- homes_y) homes_kid_2_y) 10.0))))
 (let (($x1948 (>= (- (+ (- homes_x homes_kid_2_x) homes_width) homes_kid_2_width) 10.0)))
 (let (($x1949 (or $x1908 $x1948)))
 (let (($x1944 (or $x1908 (>= (+ (- homes_x) homes_kid_2_x) 10.0))))
 (let (($x1940 (>= (- (- (+ homes_y homes_hight) homes_kid_1_y) homes_kid_1_hight) 10.0)))
 (let (($x1941 (or $x1908 $x1940)))
 (let (($x1937 (or $x1908 (>= (+ (- homes_y) homes_kid_1_y) 10.0))))
 (let ((?x1932 (- (+ (+ (- homes_kid_1_width) homes_x) homes_width) homes_kid_1_x)))
 (let (($x1934 (or $x1908 (>= ?x1932 10.0))))
 (let (($x1928 (or $x1908 (>= (+ (- homes_x) homes_kid_1_x) 10.0))))
 (let (($x1924 (>= (- (- (+ homes_y homes_hight) homes_kid_0_y) homes_kid_0_hight) 10.0)))
 (let (($x1925 (or $x1908 $x1924)))
 (let (($x1920 (or $x1908 (>= (+ (- homes_y) homes_kid_0_y) 10.0))))
 (let ((?x1915 (- (+ (+ (- homes_kid_0_width) homes_x) homes_width) homes_kid_0_x)))
 (let (($x1917 (or $x1908 (>= ?x1915 10.0))))
 (let (($x1911 (or $x1908 (>= (+ (- homes_x) homes_kid_0_x) 10.0))))
 (let (($x1907 (>= homes_kid_3_hight 0.0)))
 (let (($x1906 (>= homes_kid_3_width 0.0)))
 (let (($x1905 (>= homes_kid_3_y 0.0)))
 (let (($x1904 (>= homes_kid_3_x 0.0)))
 (let (($x1903 (>= homes_kid_2_hight 0.0)))
 (let (($x1902 (>= homes_kid_2_width 0.0)))
 (let (($x1901 (>= homes_kid_2_y 0.0)))
 (let (($x1900 (>= homes_kid_2_x 0.0)))
 (let (($x1899 (>= homes_kid_1_hight 0.0)))
 (let (($x1898 (>= homes_kid_1_width 0.0)))
 (let (($x1897 (>= homes_kid_1_y 0.0)))
 (let (($x1896 (>= homes_kid_1_x 0.0)))
 (let (($x1895 (>= homes_kid_0_hight 0.0)))
 (let (($x1894 (>= homes_kid_0_width 0.0)))
 (let (($x1893 (>= homes_kid_0_y 0.0)))
 (let (($x1892 (>= homes_kid_0_x 0.0)))
 (let (($x1891 (or $x1825 (= menus_kid_0_width 100.0))))
 (let (($x1889 (or $x1825 (= (+ (- menus_kid_1_width) menus_kid_0_width) 0.0))))
 (let ((?x1883 (* 2.0 menus_kid_1_x)))
 (let (($x1885 (= (+ (- (- menus_kid_1_width (* 2.0 menus_x)) menus_width) ?x1883) 0.0)))
 (let (($x1886 (or $x1825 $x1885)))
 (let (($x1879 (or $x1825 (= (- menus_kid_0_x menus_x) 10.0))))
 (let ((?x1875 (+ (+ (- (- menus_y) menus_hight) menus_kid_1_y) menus_kid_1_hight)))
 (let (($x1877 (or $x1825 (= ?x1875 (- 10.0)))))
 (let (($x1872 (or $x1825 (= (+ (- menus_y) menus_kid_1_y) 10.0))))
 (let ((?x1868 (+ (- (+ (- menus_y) menus_kid_0_hight) menus_hight) menus_kid_0_y)))
 (let (($x1870 (or $x1825 (= ?x1868 (- 10.0)))))
 (let (($x1865 (or $x1825 (= (+ (- menus_y) menus_kid_0_y) 10.0))))
 (let (($x1862 (>= (+ (- (- menus_kid_0_x) menus_kid_0_width) menus_kid_1_x) 0.0)))
 (let (($x1863 (or $x1825 $x1862)))
 (let (($x1858 (>= (- (- (+ menus_y menus_hight) menus_kid_1_y) menus_kid_1_hight) 10.0)))
 (let (($x1859 (or $x1825 $x1858)))
 (let (($x1854 (or $x1825 (>= (+ (- menus_y) menus_kid_1_y) 10.0))))
 (let ((?x1849 (- (+ (+ (- menus_kid_1_width) menus_x) menus_width) menus_kid_1_x)))
 (let (($x1851 (or $x1825 (>= ?x1849 10.0))))
 (let (($x1845 (or $x1825 (>= (+ (- menus_x) menus_kid_1_x) 10.0))))
 (let (($x1841 (>= (- (+ (- menus_y menus_kid_0_hight) menus_hight) menus_kid_0_y) 10.0)))
 (let (($x1842 (or $x1825 $x1841)))
 (let (($x1837 (or $x1825 (>= (+ (- menus_y) menus_kid_0_y) 10.0))))
 (let ((?x1832 (+ (- (+ (- menus_kid_0_x) menus_x) menus_kid_0_width) menus_width)))
 (let (($x1834 (or $x1825 (>= ?x1832 10.0))))
 (let (($x1828 (or $x1825 (>= (- menus_kid_0_x menus_x) 10.0))))
 (let (($x1824 (>= menus_kid_1_hight 0.0)))
 (let (($x1823 (>= menus_kid_1_width 0.0)))
 (let (($x1822 (>= menus_kid_1_y 0.0)))
 (let (($x1821 (>= menus_kid_1_x 0.0)))
 (let (($x1820 (>= menus_kid_0_hight 0.0)))
 (let (($x1819 (>= menus_kid_0_width 0.0)))
 (let (($x1818 (>= menus_kid_0_y 0.0)))
 (let (($x1817 (>= menus_kid_0_x 0.0)))
 (let (($x1816 (= (+ (- (+ (- ads_x) ads_top_2_x) ads_width) ads_top_2_width) 0.0)))
 (let ((?x490 (- ads_x)))
 (let ((?x1812 (+ ?x490 ads_top_2_x)))
 (let (($x1813 (= ?x1812 0.0)))
 (let (($x1811 (or $x1532 (= (+ (- homes_hight) menus_hight) 0.0))))
 (let (($x1807 (or $x1532 (= (- (+ (- menus_y) homes_y) menus_hight) 0.0))))
 (let (($x1804 (= (- (+ (- homes_y ads_top_2_y) homes_hight) ads_top_2_hight) 0.0)))
 (let (($x1805 (or $x1532 $x1804)))
 (let (($x1801 (or $x1532 (= (- menus_y ads_top_2_y) 0.0))))
 (let (($x1798 (= (- (+ (- homes_x ads_top_2_x) homes_width) ads_top_2_width) 0.0)))
 (let (($x1799 (or $x1532 $x1798)))
 (let (($x1794 (= (+ (- (- menus_x ads_top_2_x) ads_top_2_width) menus_width) 0.0)))
 (let (($x1795 (or $x1532 $x1794)))
 (let (($x1791 (or $x1532 (= (- homes_x ads_top_2_x) 0.0))))
 (let (($x1789 (or $x1532 (= (- menus_x ads_top_2_x) 0.0))))
 (let (($x1787 (= ads_top_2_hight 100.0)))
 (let (($x1786 (or $x1532 (>= (- (+ (- menus_y) homes_y) menus_hight) 0.0))))
 (let (($x1781 (>= (+ (- (+ (- homes_y) ads_top_2_y) homes_hight) ads_top_2_hight) 0.0)))
 (let (($x1782 (or $x1532 $x1781)))
 (let (($x1776 (or $x1532 (>= (- homes_y ads_top_2_y) 0.0))))
 (let (($x1772 (>= (+ (- (+ (- homes_x) ads_top_2_x) homes_width) ads_top_2_width) 0.0)))
 (let (($x1773 (or $x1532 $x1772)))
 (let (($x1767 (or $x1532 (>= (- homes_x ads_top_2_x) 0.0))))
 (let (($x1763 (>= (- (+ (+ (- menus_y) ads_top_2_y) ads_top_2_hight) menus_hight) 0.0)))
 (let (($x1764 (or $x1532 $x1763)))
 (let (($x1758 (or $x1532 (>= (- menus_y ads_top_2_y) 0.0))))
 (let (($x1754 (>= (- (+ (+ (- menus_x) ads_top_2_x) ads_top_2_width) menus_width) 0.0)))
 (let (($x1755 (or $x1532 $x1754)))
 (let (($x1749 (or $x1532 (>= (- menus_x ads_top_2_x) 0.0))))
 (let (($x1746 (>= homes_hight 0.0)))
 (let (($x1745 (>= homes_width 0.0)))
 (let (($x1744 (>= homes_y 0.0)))
 (let (($x1743 (>= homes_x 0.0)))
 (let (($x1742 (>= menus_hight 0.0)))
 (let (($x1741 (>= menus_width 0.0)))
 (let (($x1740 (>= menus_y 0.0)))
 (let (($x1739 (>= menus_x 0.0)))
 (let (($x1738 (or $x1517 (= prime_top_width 100.0))))
 (let (($x1736 (or $x1517 (= (- prime_top_width ads_top_1_kid_4_width) 0.0))))
 (let (($x1733 (or $x1517 (= (+ (- categories_width) prime_top_width) 0.0))))
 (let (($x1730 (or $x1517 (= (+ (- store_width) prime_top_width) 0.0))))
 (let (($x1726 (or $x1517 (= (+ (- home_width) prime_top_width) 0.0))))
 (let (($x1722 (= ads_top_1_hight 50.0)))
 (let ((?x1719 (+ (- (+ (* (- 2.0) ads_x) (* 2.0 ads_top_1_x)) ads_width) ads_top_1_width)))
 (let (($x1721 (or $x1517 (= ?x1719 0.0))))
 (let ((?x1632 (- (+ (- categories_width) ads_top_1_kid_4_x) categories_x)))
 (let (($x1714 (or $x1517 (>= ?x1632 0.0))))
 (let (($x1712 (or $x1517 (>= (+ (- (- store_x) store_width) categories_x) 0.0))))
 (let (($x1710 (or $x1517 (>= (- (+ (- home_x) store_x) home_width) 0.0))))
 (let (($x1708 (or $x1517 (>= (- (- home_x prime_top_x) prime_top_width) 0.0))))
 (let ((?x1704 (+ (- (- ads_top_1_y ads_top_1_kid_4_y) ads_top_1_kid_4_hight) ads_top_1_hight)))
 (let (($x1706 (or $x1517 (>= ?x1704 10.0))))
 (let (($x1701 (or $x1517 (>= (+ (- ads_top_1_y) ads_top_1_kid_4_y) 10.0))))
 (let ((?x1697 (+ (- (- ads_top_1_x ads_top_1_kid_4_x) ads_top_1_kid_4_width) ads_top_1_width)))
 (let (($x1699 (or $x1517 (>= ?x1697 10.0))))
 (let (($x1694 (or $x1517 (>= (+ (- ads_top_1_x) ads_top_1_kid_4_x) 10.0))))
 (let ((?x1690 (- (+ (- ads_top_1_y categories_y) ads_top_1_hight) categories_hight)))
 (let (($x1692 (or $x1517 (>= ?x1690 10.0))))
 (let (($x1687 (or $x1517 (>= (+ (- ads_top_1_y) categories_y) 10.0))))
 (let ((?x1683 (+ (- (+ (- categories_width) ads_top_1_x) categories_x) ads_top_1_width)))
 (let (($x1685 (or $x1517 (>= ?x1683 10.0))))
 (let (($x1680 (or $x1517 (>= (+ (- ads_top_1_x) categories_x) 10.0))))
 (let (($x1676 (>= (- (- (+ ads_top_1_y ads_top_1_hight) store_y) store_hight) 10.0)))
 (let (($x1677 (or $x1517 $x1676)))
 (let (($x1673 (or $x1517 (>= (+ (- ads_top_1_y) store_y) 10.0))))
 (let (($x1670 (>= (+ (+ (- (- store_x) store_width) ads_top_1_x) ads_top_1_width) 10.0)))
 (let (($x1671 (or $x1517 $x1670)))
 (let (($x1667 (or $x1517 (>= (- store_x ads_top_1_x) 10.0))))
 (let (($x1663 (>= (- (- (+ ads_top_1_y ads_top_1_hight) home_y) home_hight) 10.0)))
 (let (($x1664 (or $x1517 $x1663)))
 (let (($x1659 (or $x1517 (>= (+ (- ads_top_1_y) home_y) 10.0))))
 (let (($x1656 (>= (+ (+ (- (- home_x) home_width) ads_top_1_x) ads_top_1_width) 10.0)))
 (let (($x1657 (or $x1517 $x1656)))
 (let (($x1652 (or $x1517 (>= (- home_x ads_top_1_x) 10.0))))
 (let ((?x1647 (- (+ (- ads_top_1_y prime_top_hight) ads_top_1_hight) prime_top_y)))
 (let (($x1649 (or $x1517 (>= ?x1647 10.0))))
 (let (($x1644 (or $x1517 (>= (+ (- ads_top_1_y) prime_top_y) 10.0))))
 (let ((?x1640 (+ (- (+ (- prime_top_x) ads_top_1_x) prime_top_width) ads_top_1_width)))
 (let (($x1642 (or $x1517 (>= ?x1640 10.0))))
 (let (($x1636 (or $x1517 (>= (- prime_top_x ads_top_1_x) 10.0))))
 (let (($x1634 (or $x1517 (= ?x1632 30.0))))
 (let (($x1629 (or $x1517 (= (+ (- (- store_x) store_width) categories_x) 30.0))))
 (let (($x1624 (or $x1517 (= (- (+ (- home_x) store_x) home_width) 30.0))))
 (let (($x1619 (or $x1517 (= (- (- home_x prime_top_x) prime_top_width) 30.0))))
 (let ((?x1613 (- (+ (+ (- ads_top_1_y) ads_top_1_kid_4_y) ads_top_1_kid_4_hight) ads_top_1_hight)))
 (let (($x1615 (or $x1517 (= ?x1613 (- 10.0)))))
 (let ((?x1609 (+ (- (+ (- ads_top_1_y) categories_y) ads_top_1_hight) categories_hight)))
 (let (($x1611 (or $x1517 (= ?x1609 (- 10.0)))))
 (let (($x1606 (= (+ (+ (- (- ads_top_1_y) ads_top_1_hight) store_y) store_hight) (- 10.0))))
 (let (($x1607 (or $x1517 $x1606)))
 (let (($x1602 (= (+ (+ (- (- ads_top_1_y) ads_top_1_hight) home_y) home_hight) (- 10.0))))
 (let (($x1603 (or $x1517 $x1602)))
 (let ((?x1596 (+ (- (+ (- ads_top_1_y) prime_top_hight) ads_top_1_hight) prime_top_y)))
 (let (($x1598 (or $x1517 (= ?x1596 (- 10.0)))))
 (let (($x1593 (or $x1517 (= (+ (- ads_top_1_y) ads_top_1_kid_4_y) 10.0))))
 (let (($x1590 (or $x1517 (= (+ (- ads_top_1_y) categories_y) 10.0))))
 (let (($x1587 (or $x1517 (= (+ (- ads_top_1_y) store_y) 10.0))))
 (let (($x1584 (or $x1517 (= (+ (- ads_top_1_y) home_y) 10.0))))
 (let (($x1581 (or $x1517 (= (+ (- ads_top_1_y) prime_top_y) 10.0))))
 (let ((?x1575 (- (+ (+ (- ads_top_1_x) ads_top_1_kid_4_x) ads_top_1_kid_4_width) ads_top_1_width)))
 (let (($x1577 (or $x1517 (= ?x1575 (- 10.0)))))
 (let (($x1571 (or $x1517 (= (- prime_top_x ads_top_1_x) 10.0))))
 (let (($x1568 (>= ads_top_1_kid_4_hight 0.0)))
 (let (($x1567 (>= ads_top_1_kid_4_width 0.0)))
 (let (($x1566 (>= ads_top_1_kid_4_y 0.0)))
 (let (($x1565 (>= ads_top_1_kid_4_x 0.0)))
 (let (($x1564 (>= categories_hight 0.0)))
 (let (($x1563 (>= categories_width 0.0)))
 (let (($x1562 (>= categories_y 0.0)))
 (let (($x1561 (>= categories_x 0.0)))
 (let (($x1560 (>= store_hight 0.0)))
 (let (($x1559 (>= store_width 0.0)))
 (let (($x1558 (>= store_y 0.0)))
 (let (($x1557 (>= store_x 0.0)))
 (let (($x1556 (>= home_hight 0.0)))
 (let (($x1555 (>= home_width 0.0)))
 (let (($x1554 (>= home_y 0.0)))
 (let (($x1553 (>= home_x 0.0)))
 (let (($x1552 (>= prime_top_hight 0.0)))
 (let (($x1551 (>= prime_top_width 0.0)))
 (let (($x1550 (>= prime_top_y 0.0)))
 (let (($x1549 (>= prime_top_x 0.0)))
 (let (($x1548 (or $x1517 $x1532)))
 (let (($x1547 (or ads_top_1_feasible ads_top_2_feasible)))
 (let ((?x1544 (- (+ (- ads_top_2_y ads_top_holder_y) ads_top_2_hight) ads_top_holder_hight)))
 (let (($x1546 (or $x1532 (= ?x1544 0.0))))
 (let (($x1542 (or $x1532 (= (- ads_top_2_y ads_top_holder_y) 0.0))))
 (let ((?x1537 (- (+ (- ads_top_2_x ads_top_holder_x) ads_top_2_width) ads_top_holder_width)))
 (let (($x1539 (or $x1532 (= ?x1537 0.0))))
 (let (($x1535 (or $x1532 (= (- ads_top_2_x ads_top_holder_x) 0.0))))
 (let ((?x1529 (+ (- (- ads_top_1_y ads_top_holder_y) ads_top_holder_hight) ads_top_1_hight)))
 (let (($x1531 (or $x1517 (= ?x1529 0.0))))
 (let (($x1527 (or $x1517 (= (- ads_top_1_y ads_top_holder_y) 0.0))))
 (let ((?x1522 (+ (- (- ads_top_1_x ads_top_holder_x) ads_top_holder_width) ads_top_1_width)))
 (let (($x1524 (or $x1517 (= ?x1522 0.0))))
 (let (($x1520 (or $x1517 (= (- ads_top_1_x ads_top_holder_x) 0.0))))
 (let (($x1516 (>= ads_top_2_hight 0.0)))
 (let (($x1515 (>= ads_top_2_width 0.0)))
 (let (($x1514 (>= ads_top_2_y 0.0)))
 (let (($x1513 (>= ads_top_2_x 0.0)))
 (let (($x1512 (>= ads_top_1_hight 0.0)))
 (let (($x1511 (>= ads_top_1_width 0.0)))
 (let (($x1510 (>= ads_top_1_y 0.0)))
 (let (($x1509 (>= ads_top_1_x 0.0)))
 (let ((?x1505 (+ (+ (- ads_pics_2_hight) left_buttons_watch_y) left_buttons_watch_hight)))
 (let (($x1508 (or $x1299 (= (- ?x1505 ads_pics_2_y) 0.0))))
 (let ((?x1412 (- (- left_buttons_watch_y left_buttons_title_y) left_buttons_title_hight)))
 (let (($x1502 (or $x1299 (= ?x1412 0.0))))
 (let (($x1500 (or $x1299 (= (+ (- ads_pics_2_x) left_buttons_watch_x) 40.0))))
 (let (($x1498 (or $x1299 (= (- left_buttons_title_x ads_pics_2_x) 40.0))))
 (let (($x1413 (>= ?x1412 0.0)))
 (let (($x1496 (or $x1299 $x1413)))
 (let ((?x1492 (- (- ads_pics_2_hight left_buttons_watch_y) left_buttons_watch_hight)))
 (let (($x1495 (or $x1299 (>= (+ ?x1492 ads_pics_2_y) 0.0))))
 (let (($x1490 (or $x1299 (>= (- left_buttons_watch_y ads_pics_2_y) 0.0))))
 (let ((?x1485 (- (+ (+ (- left_buttons_watch_width) ads_pics_2_x) ads_pics_2_width) left_buttons_watch_x)))
 (let (($x1487 (or $x1299 (>= ?x1485 0.0))))
 (let (($x1482 (or $x1299 (>= (+ (- ads_pics_2_x) left_buttons_watch_x) 0.0))))
 (let ((?x1476 (- (+ (- ads_pics_2_hight left_buttons_title_y) ads_pics_2_y) left_buttons_title_hight)))
 (let (($x1478 (or $x1299 (>= ?x1476 0.0))))
 (let (($x1473 (or $x1299 (>= (- left_buttons_title_y ads_pics_2_y) 0.0))))
 (let ((?x1467 (- (+ (- left_buttons_title_x) ads_pics_2_x) left_buttons_title_width)))
 (let (($x1470 (or $x1299 (>= (+ ?x1467 ads_pics_2_width) 0.0))))
 (let (($x1465 (or $x1299 (>= (- left_buttons_title_x ads_pics_2_x) 0.0))))
 (let ((?x1416 (- (- left_buttons_detail_y left_buttons_watch_y) left_buttons_watch_hight)))
 (let (($x1462 (or $x1283 (= ?x1416 0.0))))
 (let (($x1460 (= (+ (- 60.0) left_buttons_detail_hight) 0.0)))
 (let (($x1457 (= (+ (- 130.0) left_buttons_detail_width) 0.0)))
 (let ((?x1452 (- (- (+ (- 20.0) left_buttons_watch_y) left_buttons_title_y) left_buttons_title_hight)))
 (let (($x1454 (or $x1283 (= ?x1452 0.0))))
 (let (($x1448 (= (+ (- 80.0) left_buttons_watch_hight) 0.0)))
 (let (($x1445 (= (+ (- 600.0) left_buttons_watch_width) 0.0)))
 (let (($x1442 (= (+ (- left_buttons_title_width) (* 5.0 left_buttons_title_hight)) 0.0)))
 (let ((?x1436 (* 2.0 ads_pics_holder_width)))
 (let ((?x1434 (* 5.0 left_buttons_title_width)))
 (let (($x1438 (= (- ?x1434 ?x1436) 0.0)))
 (let (($x1432 (or $x1283 (= (+ (- ads_pics_x) left_buttons_detail_x) 40.0))))
 (let (($x1430 (or $x1283 (= (+ (- ads_pics_x) left_buttons_watch_x) 40.0))))
 (let (($x1428 (or $x1283 (= (- left_buttons_title_x ads_pics_x) 40.0))))
 (let ((?x1423 (+ (- (+ (* (- 2.0) ads_pics_y) left_buttons_detail_y) ads_pics_hight) left_buttons_detail_hight)))
 (let (($x1425 (= (+ ?x1423 left_buttons_title_y) 0.0)))
 (let (($x1418 (or $x1283 (>= ?x1416 0.0))))
 (let (($x1414 (or $x1283 $x1413)))
 (let ((?x1408 (- (+ (- ads_pics_y left_buttons_detail_y) ads_pics_hight) left_buttons_detail_hight)))
 (let (($x1410 (or $x1283 (>= ?x1408 0.0))))
 (let (($x1405 (or $x1283 (>= (+ (- ads_pics_y) left_buttons_detail_y) 0.0))))
 (let ((?x1400 (- (+ (- ads_pics_x left_buttons_detail_x) ads_pics_width) left_buttons_detail_width)))
 (let (($x1402 (or $x1283 (>= ?x1400 0.0))))
 (let (($x1397 (or $x1283 (>= (+ (- ads_pics_x) left_buttons_detail_x) 0.0))))
 (let ((?x1392 (- (- (+ ads_pics_y ads_pics_hight) left_buttons_watch_y) left_buttons_watch_hight)))
 (let (($x1394 (or $x1283 (>= ?x1392 0.0))))
 (let (($x1390 (or $x1283 (>= (+ (- ads_pics_y) left_buttons_watch_y) 0.0))))
 (let ((?x1385 (- (+ (+ (- left_buttons_watch_width) ads_pics_x) ads_pics_width) left_buttons_watch_x)))
 (let (($x1387 (or $x1283 (>= ?x1385 0.0))))
 (let (($x1381 (or $x1283 (>= (+ (- ads_pics_x) left_buttons_watch_x) 0.0))))
 (let ((?x1375 (- (- (+ ads_pics_y ads_pics_hight) left_buttons_title_y) left_buttons_title_hight)))
 (let (($x1377 (or $x1283 (>= ?x1375 0.0))))
 (let (($x1372 (or $x1283 (>= (+ (- ads_pics_y) left_buttons_title_y) 0.0))))
 (let ((?x1366 (+ (+ (- (- left_buttons_title_x) left_buttons_title_width) ads_pics_x) ads_pics_width)))
 (let (($x1368 (or $x1283 (>= ?x1366 0.0))))
 (let (($x1362 (or $x1283 (>= (- left_buttons_title_x ads_pics_x) 0.0))))
 (let (($x1359 (>= left_buttons_detail_hight 0.0)))
 (let (($x1358 (>= left_buttons_detail_width 0.0)))
 (let (($x1357 (>= left_buttons_detail_y 0.0)))
 (let (($x1356 (>= left_buttons_detail_x 0.0)))
 (let (($x1355 (>= left_buttons_watch_hight 0.0)))
 (let (($x1354 (>= left_buttons_watch_width 0.0)))
 (let (($x1353 (>= left_buttons_watch_y 0.0)))
 (let (($x1352 (>= left_buttons_watch_x 0.0)))
 (let (($x1351 (>= left_buttons_title_hight 0.0)))
 (let (($x1350 (>= left_buttons_title_width 0.0)))
 (let (($x1349 (>= left_buttons_title_y 0.0)))
 (let (($x1348 (>= left_buttons_title_x 0.0)))
 (let (($x1347 (= (- (* 10.0 ads_pics_holder_hight) (* 3.0 ads_pics_holder_width)) 0.0)))
 (let (($x1342 (= (+ (- (+ ?x490 ads_pics_holder_x) ads_width) ads_pics_holder_width) (- 30.0))))
 (let ((?x1255 (+ ?x490 ads_pics_holder_x)))
 (let (($x1338 (= ?x1255 30.0)))
 (let (($x1316 (not ads_pics_3_feasible)))
 (let (($x1336 (or $x1299 $x1316)))
 (let (($x1335 (or $x1283 $x1316)))
 (let (($x1334 (or $x1283 $x1299)))
 (let (($x1333 (or ads_pics_feasible ads_pics_2_feasible ads_pics_3_feasible)))
 (let ((?x1330 (+ (+ (- (- ads_pics_holder_y) ads_pics_holder_hight) ads_pics_3_y) ads_pics_3_hight)))
 (let (($x1332 (or $x1316 (= ?x1330 0.0))))
 (let (($x1327 (or $x1316 (= (+ (- ads_pics_holder_y) ads_pics_3_y) 0.0))))
 (let ((?x1322 (- (- (+ ads_pics_3_x ads_pics_3_width) ads_pics_holder_x) ads_pics_holder_width)))
 (let (($x1324 (or $x1316 (= ?x1322 0.0))))
 (let (($x1319 (or $x1316 (= (- ads_pics_3_x ads_pics_holder_x) 0.0))))
 (let ((?x1313 (+ (- (- ads_pics_2_hight ads_pics_holder_y) ads_pics_holder_hight) ads_pics_2_y)))
 (let (($x1315 (or $x1299 (= ?x1313 0.0))))
 (let (($x1310 (or $x1299 (= (+ (- ads_pics_holder_y) ads_pics_2_y) 0.0))))
 (let ((?x1304 (- (+ (- ads_pics_2_x ads_pics_holder_x) ads_pics_2_width) ads_pics_holder_width)))
 (let (($x1306 (or $x1299 (= ?x1304 0.0))))
 (let (($x1302 (or $x1299 (= (- ads_pics_2_x ads_pics_holder_x) 0.0))))
 (let ((?x1296 (- (+ (- ads_pics_y ads_pics_holder_y) ads_pics_hight) ads_pics_holder_hight)))
 (let (($x1298 (or $x1283 (= ?x1296 0.0))))
 (let (($x1294 (or $x1283 (= (- ads_pics_y ads_pics_holder_y) 0.0))))
 (let ((?x1289 (- (+ (+ (- ads_pics_holder_x) ads_pics_x) ads_pics_width) ads_pics_holder_width)))
 (let (($x1291 (or $x1283 (= ?x1289 0.0))))
 (let (($x1287 (or $x1283 (= (+ (- ads_pics_holder_x) ads_pics_x) 0.0))))
 (let (($x1282 (>= ads_pics_3_hight 0.0)))
 (let (($x1281 (>= ads_pics_3_width 0.0)))
 (let (($x1280 (>= ads_pics_3_y 0.0)))
 (let (($x1279 (>= ads_pics_3_x 0.0)))
 (let (($x1278 (>= ads_pics_2_hight 0.0)))
 (let (($x1277 (>= ads_pics_2_width 0.0)))
 (let (($x1276 (>= ads_pics_2_y 0.0)))
 (let (($x1275 (>= ads_pics_2_x 0.0)))
 (let (($x1274 (>= ads_pics_hight 0.0)))
 (let (($x1273 (>= ads_pics_width 0.0)))
 (let (($x1272 (>= ads_pics_y 0.0)))
 (let (($x1271 (>= ads_pics_x 0.0)))
 (let (($x1270 (>= (- (+ (- ads_top_holder_y) ads_pics_holder_y) ads_top_holder_hight) 0.0)))
 (let ((?x1265 (- (+ (- ads_y ads_pics_holder_y) ads_hight) ads_pics_holder_hight)))
 (let (($x1266 (>= ?x1265 0.0)))
 (let (($x1262 (>= (+ (- ads_y) ads_pics_holder_y) 0.0)))
 (let ((?x1259 (- (+ (- ads_x ads_pics_holder_x) ads_width) ads_pics_holder_width)))
 (let (($x1260 (>= ?x1259 0.0)))
 (let (($x1256 (>= ?x1255 0.0)))
 (let (($x1254 (>= (- (+ (- ads_y ads_top_holder_y) ads_hight) ads_top_holder_hight) 0.0)))
 (let (($x1250 (>= (+ (- ads_y) ads_top_holder_y) 0.0)))
 (let (($x1248 (>= (- (+ (- ads_x ads_top_holder_x) ads_width) ads_top_holder_width) 0.0)))
 (let (($x1244 (>= (+ ?x490 ads_top_holder_x) 0.0)))
 (let (($x1242 (>= ads_pics_holder_hight 0.0)))
 (let (($x1241 (>= ads_pics_holder_width 0.0)))
 (let (($x1240 (>= ads_pics_holder_y 0.0)))
 (let (($x1239 (>= ads_pics_holder_x 0.0)))
 (let (($x1238 (>= ads_top_holder_hight 0.0)))
 (let (($x1237 (>= ads_top_holder_width 0.0)))
 (let (($x1236 (>= ads_top_holder_y 0.0)))
 (let (($x1235 (>= ads_top_holder_x 0.0)))
 (let ((?x1229 (+ (- (+ (- buttons_width) buttons_kid_16_width) buttons_x) buttons_kid_16_x)))
 (let (($x1230 (<= ?x1229 0.0)))
 (let (($x1233 (not buttons_kid_16_feasible)))
 (let (($x1234 (or $x1233 $x1230)))
 (let (($x1232 (or (not $x1230) buttons_kid_16_feasible)))
 (let ((?x1221 (- (+ (+ (- buttons_width) buttons_kid_15_x) buttons_kid_15_width) buttons_x)))
 (let (($x1222 (<= ?x1221 0.0)))
 (let (($x1225 (not buttons_kid_15_feasible)))
 (let (($x1226 (or $x1225 $x1222)))
 (let (($x1224 (or (not $x1222) buttons_kid_15_feasible)))
 (let ((?x1213 (- (+ (+ (- buttons_width) buttons_kid_14_x) buttons_kid_14_width) buttons_x)))
 (let (($x1214 (<= ?x1213 0.0)))
 (let (($x1217 (not buttons_kid_14_feasible)))
 (let (($x1218 (or $x1217 $x1214)))
 (let (($x1216 (or (not $x1214) buttons_kid_14_feasible)))
 (let ((?x1205 (- (+ (+ (- buttons_width) buttons_kid_13_x) buttons_kid_13_width) buttons_x)))
 (let (($x1206 (<= ?x1205 0.0)))
 (let (($x1209 (not buttons_kid_13_feasible)))
 (let (($x1210 (or $x1209 $x1206)))
 (let (($x1208 (or (not $x1206) buttons_kid_13_feasible)))
 (let ((?x1197 (- (+ (+ (- buttons_width) buttons_kid_12_x) buttons_kid_12_width) buttons_x)))
 (let (($x1198 (<= ?x1197 0.0)))
 (let (($x1201 (not buttons_kid_12_feasible)))
 (let (($x1202 (or $x1201 $x1198)))
 (let (($x1200 (or (not $x1198) buttons_kid_12_feasible)))
 (let ((?x1189 (- (+ (- buttons_kid_11_width buttons_width) buttons_kid_11_x) buttons_x)))
 (let (($x1190 (<= ?x1189 0.0)))
 (let (($x1193 (not buttons_kid_11_feasible)))
 (let (($x1194 (or $x1193 $x1190)))
 (let (($x1192 (or (not $x1190) buttons_kid_11_feasible)))
 (let ((?x1181 (+ (- (+ (- buttons_width) buttons_kid_10_x) buttons_x) buttons_kid_10_width)))
 (let (($x1182 (<= ?x1181 0.0)))
 (let (($x1185 (not buttons_kid_10_feasible)))
 (let (($x1186 (or $x1185 $x1182)))
 (let (($x1184 (or (not $x1182) buttons_kid_10_feasible)))
 (let ((?x1173 (+ (- (+ (- buttons_width) buttons_kid_9_width) buttons_x) buttons_kid_9_x)))
 (let (($x1174 (<= ?x1173 0.0)))
 (let (($x1177 (not buttons_kid_9_feasible)))
 (let (($x1178 (or $x1177 $x1174)))
 (let (($x1176 (or (not $x1174) buttons_kid_9_feasible)))
 (let ((?x1165 (- (+ (+ (- buttons_width) buttons_kid_8_x) buttons_kid_8_width) buttons_x)))
 (let (($x1166 (<= ?x1165 0.0)))
 (let (($x1169 (not buttons_kid_8_feasible)))
 (let (($x1170 (or $x1169 $x1166)))
 (let (($x1168 (or (not $x1166) buttons_kid_8_feasible)))
 (let ((?x1157 (- (+ (+ (- buttons_width) buttons_kid_7_x) buttons_kid_7_width) buttons_x)))
 (let (($x1158 (<= ?x1157 0.0)))
 (let (($x1161 (not buttons_kid_7_feasible)))
 (let (($x1162 (or $x1161 $x1158)))
 (let (($x1160 (or (not $x1158) buttons_kid_7_feasible)))
 (let ((?x1149 (- (+ (+ (- buttons_width) buttons_kid_6_x) buttons_kid_6_width) buttons_x)))
 (let (($x1150 (<= ?x1149 0.0)))
 (let (($x1153 (not buttons_kid_6_feasible)))
 (let (($x1154 (or $x1153 $x1150)))
 (let (($x1152 (or (not $x1150) buttons_kid_6_feasible)))
 (let ((?x1141 (- (+ (+ (- buttons_width) buttons_kid_5_x) buttons_kid_5_width) buttons_x)))
 (let (($x1142 (<= ?x1141 0.0)))
 (let (($x1145 (not buttons_kid_5_feasible)))
 (let (($x1146 (or $x1145 $x1142)))
 (let (($x1144 (or (not $x1142) buttons_kid_5_feasible)))
 (let ((?x1133 (- (+ (- buttons_kid_4_width buttons_width) buttons_kid_4_x) buttons_x)))
 (let (($x1134 (<= ?x1133 0.0)))
 (let (($x1137 (not buttons_kid_4_feasible)))
 (let (($x1138 (or $x1137 $x1134)))
 (let (($x1136 (or (not $x1134) buttons_kid_4_feasible)))
 (let ((?x1125 (- (+ (- buttons_kid_3_width buttons_width) buttons_kid_3_x) buttons_x)))
 (let (($x1126 (<= ?x1125 0.0)))
 (let (($x1129 (not buttons_kid_3_feasible)))
 (let (($x1130 (or $x1129 $x1126)))
 (let (($x1128 (or (not $x1126) buttons_kid_3_feasible)))
 (let ((?x1117 (+ (- (+ (- buttons_width) buttons_kid_2_width) buttons_x) buttons_kid_2_x)))
 (let (($x1118 (<= ?x1117 0.0)))
 (let (($x1121 (not buttons_kid_2_feasible)))
 (let (($x1122 (or $x1121 $x1118)))
 (let (($x1120 (or (not $x1118) buttons_kid_2_feasible)))
 (let ((?x1109 (- (+ (+ (- buttons_width) buttons_kid_1_x) buttons_kid_1_width) buttons_x)))
 (let (($x1110 (<= ?x1109 0.0)))
 (let (($x1113 (not buttons_kid_1_feasible)))
 (let (($x1114 (or $x1113 $x1110)))
 (let (($x1112 (or (not $x1110) buttons_kid_1_feasible)))
 (let ((?x1101 (- (+ (+ (- buttons_width) buttons_kid_0_x) buttons_kid_0_width) buttons_x)))
 (let (($x1102 (<= ?x1101 0.0)))
 (let (($x1105 (not buttons_kid_0_feasible)))
 (let (($x1106 (or $x1105 $x1102)))
 (let (($x1104 (or (not $x1102) buttons_kid_0_feasible)))
 (let ((?x1097 (+ (- (- (- 10.0) buttons_kid_15_x) buttons_kid_15_width) buttons_kid_16_x)))
 (let (($x1098 (= ?x1097 0.0)))
 (let ((?x1093 (- (+ (- (- 10.0) buttons_kid_14_x) buttons_kid_15_x) buttons_kid_14_width)))
 (let (($x1094 (= ?x1093 0.0)))
 (let ((?x1089 (- (- (+ (- 10.0) buttons_kid_14_x) buttons_kid_13_x) buttons_kid_13_width)))
 (let (($x1090 (= ?x1089 0.0)))
 (let ((?x1085 (- (- (+ (- 10.0) buttons_kid_13_x) buttons_kid_12_x) buttons_kid_12_width)))
 (let (($x1086 (= ?x1085 0.0)))
 (let ((?x1081 (+ (- (- (- 10.0) buttons_kid_11_width) buttons_kid_11_x) buttons_kid_12_x)))
 (let (($x1082 (= ?x1081 0.0)))
 (let ((?x1077 (- (- (+ (- 10.0) buttons_kid_11_x) buttons_kid_10_x) buttons_kid_10_width)))
 (let (($x1078 (= ?x1077 0.0)))
 (let ((?x1073 (- (+ (- (- 10.0) buttons_kid_9_width) buttons_kid_10_x) buttons_kid_9_x)))
 (let (($x1074 (= ?x1073 0.0)))
 (let ((?x1069 (+ (- (- (- 10.0) buttons_kid_8_x) buttons_kid_8_width) buttons_kid_9_x)))
 (let (($x1070 (= ?x1069 0.0)))
 (let ((?x1065 (- (+ (- (- 10.0) buttons_kid_7_x) buttons_kid_8_x) buttons_kid_7_width)))
 (let (($x1066 (= ?x1065 0.0)))
 (let ((?x1061 (- (- (+ (- 10.0) buttons_kid_7_x) buttons_kid_6_x) buttons_kid_6_width)))
 (let (($x1062 (= ?x1061 0.0)))
 (let ((?x1057 (- (- (+ (- 10.0) buttons_kid_6_x) buttons_kid_5_x) buttons_kid_5_width)))
 (let (($x1058 (= ?x1057 0.0)))
 (let ((?x1053 (- (+ (- (- 10.0) buttons_kid_4_width) buttons_kid_5_x) buttons_kid_4_x)))
 (let (($x1054 (= ?x1053 0.0)))
 (let ((?x1049 (+ (- (- (- 10.0) buttons_kid_3_width) buttons_kid_3_x) buttons_kid_4_x)))
 (let (($x1050 (= ?x1049 0.0)))
 (let ((?x1045 (- (+ (- (- 10.0) buttons_kid_2_width) buttons_kid_3_x) buttons_kid_2_x)))
 (let (($x1046 (= ?x1045 0.0)))
 (let ((?x1041 (+ (- (- (- 10.0) buttons_kid_1_x) buttons_kid_1_width) buttons_kid_2_x)))
 (let (($x1042 (= ?x1041 0.0)))
 (let ((?x1037 (- (+ (- (- 10.0) buttons_kid_0_x) buttons_kid_1_x) buttons_kid_0_width)))
 (let (($x1038 (= ?x1037 0.0)))
 (let ((?x940 (- buttons_y)))
 (let ((?x1030 (+ ?x940 buttons_kid_16_y)))
 (let (($x1034 (= ?x1030 10.0)))
 (let (($x1033 (= (+ (- ?x1030 buttons_hight) buttons_kid_16_hight) (- 10.0))))
 (let (($x1029 (= (+ ?x940 buttons_kid_15_y) 10.0)))
 (let ((?x1026 (+ (+ (- ?x940 buttons_hight) buttons_kid_15_y) buttons_kid_15_hight)))
 (let (($x1027 (= ?x1026 (- 10.0))))
 (let (($x1024 (= (+ ?x940 buttons_kid_14_y) 10.0)))
 (let ((?x1021 (+ (- (- buttons_kid_14_hight buttons_y) buttons_hight) buttons_kid_14_y)))
 (let (($x1022 (= ?x1021 (- 10.0))))
 (let (($x1018 (= (+ ?x940 buttons_kid_13_y) 10.0)))
 (let ((?x1015 (+ (- (- buttons_kid_13_hight buttons_y) buttons_hight) buttons_kid_13_y)))
 (let (($x1016 (= ?x1015 (- 10.0))))
 (let (($x1012 (= (- buttons_kid_12_y buttons_y) 10.0)))
 (let ((?x1009 (- (- (+ buttons_kid_12_y buttons_kid_12_hight) buttons_y) buttons_hight)))
 (let (($x1010 (= ?x1009 (- 10.0))))
 (let ((?x1002 (- buttons_kid_11_y buttons_y)))
 (let (($x1006 (= ?x1002 10.0)))
 (let (($x1005 (= (- (+ ?x1002 buttons_kid_11_hight) buttons_hight) (- 10.0))))
 (let ((?x997 (- buttons_kid_10_y buttons_y)))
 (let (($x1001 (= ?x997 10.0)))
 (let (($x1000 (= (- (+ ?x997 buttons_kid_10_hight) buttons_hight) (- 10.0))))
 (let ((?x992 (+ ?x940 buttons_kid_9_y)))
 (let (($x996 (= ?x992 10.0)))
 (let (($x995 (= (+ (- ?x992 buttons_hight) buttons_kid_9_hight) (- 10.0))))
 (let (($x991 (= (+ ?x940 buttons_kid_8_y) 10.0)))
 (let (($x989 (= (+ (+ (- ?x940 buttons_hight) buttons_kid_8_y) buttons_kid_8_hight) (- 10.0))))
 (let (($x985 (= (+ ?x940 buttons_kid_7_y) 10.0)))
 (let ((?x982 (+ (- (- buttons_kid_7_hight buttons_y) buttons_hight) buttons_kid_7_y)))
 (let (($x983 (= ?x982 (- 10.0))))
 (let (($x979 (= (+ ?x940 buttons_kid_6_y) 10.0)))
 (let ((?x976 (+ (- (- buttons_kid_6_hight buttons_y) buttons_hight) buttons_kid_6_y)))
 (let (($x977 (= ?x976 (- 10.0))))
 (let (($x973 (= (- buttons_kid_5_y buttons_y) 10.0)))
 (let ((?x970 (- (- (+ buttons_kid_5_y buttons_kid_5_hight) buttons_y) buttons_hight)))
 (let (($x971 (= ?x970 (- 10.0))))
 (let ((?x963 (- buttons_kid_4_y buttons_y)))
 (let (($x967 (= ?x963 10.0)))
 (let (($x966 (= (- (+ ?x963 buttons_kid_4_hight) buttons_hight) (- 10.0))))
 (let ((?x958 (- buttons_kid_3_y buttons_y)))
 (let (($x962 (= ?x958 10.0)))
 (let (($x961 (= (- (+ ?x958 buttons_kid_3_hight) buttons_hight) (- 10.0))))
 (let ((?x953 (+ ?x940 buttons_kid_2_y)))
 (let (($x957 (= ?x953 10.0)))
 (let (($x956 (= (+ (- ?x953 buttons_hight) buttons_kid_2_hight) (- 10.0))))
 (let (($x952 (= (+ ?x940 buttons_kid_1_y) 10.0)))
 (let ((?x949 (+ (- (- buttons_kid_1_hight buttons_y) buttons_hight) buttons_kid_1_y)))
 (let (($x950 (= ?x949 (- 10.0))))
 (let ((?x945 (+ (- (- buttons_kid_0_hight buttons_y) buttons_hight) buttons_kid_0_y)))
 (let (($x946 (= ?x945 (- 10.0))))
 (let (($x942 (= (+ ?x940 buttons_kid_0_y) 10.0)))
 (let (($x939 (= (- buttons_kid_0_x buttons_x) 10.0)))
 (let (($x937 (= buttons_hight 50.0)))
 (let (($x936 (= buttons_kid_16_width 100.0)))
 (let (($x935 (= buttons_kid_15_width 100.0)))
 (let (($x934 (= buttons_kid_14_width 100.0)))
 (let (($x933 (= buttons_kid_13_width 100.0)))
 (let (($x932 (= buttons_kid_12_width 100.0)))
 (let (($x931 (= buttons_kid_11_width 100.0)))
 (let (($x930 (= buttons_kid_10_width 100.0)))
 (let (($x929 (= buttons_kid_9_width 100.0)))
 (let (($x928 (= buttons_kid_8_width 100.0)))
 (let (($x927 (= buttons_kid_7_width 100.0)))
 (let (($x926 (= buttons_kid_6_width 100.0)))
 (let (($x925 (= buttons_kid_5_width 100.0)))
 (let (($x924 (= buttons_kid_4_width 100.0)))
 (let (($x923 (= buttons_kid_3_width 100.0)))
 (let (($x922 (= buttons_kid_2_width 100.0)))
 (let (($x921 (= buttons_kid_1_width 100.0)))
 (let (($x920 (= buttons_kid_0_width 100.0)))
 (let (($x918 (>= buttons_kid_16_hight 0.0)))
 (let (($x917 (>= buttons_kid_16_width 0.0)))
 (let (($x916 (>= buttons_kid_16_y 0.0)))
 (let (($x915 (>= buttons_kid_16_x 0.0)))
 (let (($x914 (>= buttons_kid_15_hight 0.0)))
 (let (($x913 (>= buttons_kid_15_width 0.0)))
 (let (($x912 (>= buttons_kid_15_y 0.0)))
 (let (($x911 (>= buttons_kid_15_x 0.0)))
 (let (($x910 (>= buttons_kid_14_hight 0.0)))
 (let (($x909 (>= buttons_kid_14_width 0.0)))
 (let (($x908 (>= buttons_kid_14_y 0.0)))
 (let (($x907 (>= buttons_kid_14_x 0.0)))
 (let (($x906 (>= buttons_kid_13_hight 0.0)))
 (let (($x905 (>= buttons_kid_13_width 0.0)))
 (let (($x904 (>= buttons_kid_13_y 0.0)))
 (let (($x903 (>= buttons_kid_13_x 0.0)))
 (let (($x902 (>= buttons_kid_12_hight 0.0)))
 (let (($x901 (>= buttons_kid_12_width 0.0)))
 (let (($x900 (>= buttons_kid_12_y 0.0)))
 (let (($x899 (>= buttons_kid_12_x 0.0)))
 (let (($x898 (>= buttons_kid_11_hight 0.0)))
 (let (($x897 (>= buttons_kid_11_width 0.0)))
 (let (($x896 (>= buttons_kid_11_y 0.0)))
 (let (($x895 (>= buttons_kid_11_x 0.0)))
 (let (($x894 (>= buttons_kid_10_hight 0.0)))
 (let (($x893 (>= buttons_kid_10_width 0.0)))
 (let (($x892 (>= buttons_kid_10_y 0.0)))
 (let (($x891 (>= buttons_kid_10_x 0.0)))
 (let (($x890 (>= buttons_kid_9_hight 0.0)))
 (let (($x889 (>= buttons_kid_9_width 0.0)))
 (let (($x888 (>= buttons_kid_9_y 0.0)))
 (let (($x887 (>= buttons_kid_9_x 0.0)))
 (let (($x886 (>= buttons_kid_8_hight 0.0)))
 (let (($x885 (>= buttons_kid_8_width 0.0)))
 (let (($x884 (>= buttons_kid_8_y 0.0)))
 (let (($x883 (>= buttons_kid_8_x 0.0)))
 (let (($x882 (>= buttons_kid_7_hight 0.0)))
 (let (($x881 (>= buttons_kid_7_width 0.0)))
 (let (($x880 (>= buttons_kid_7_y 0.0)))
 (let (($x879 (>= buttons_kid_7_x 0.0)))
 (let (($x878 (>= buttons_kid_6_hight 0.0)))
 (let (($x877 (>= buttons_kid_6_width 0.0)))
 (let (($x876 (>= buttons_kid_6_y 0.0)))
 (let (($x875 (>= buttons_kid_6_x 0.0)))
 (let (($x874 (>= buttons_kid_5_hight 0.0)))
 (let (($x873 (>= buttons_kid_5_width 0.0)))
 (let (($x872 (>= buttons_kid_5_y 0.0)))
 (let (($x871 (>= buttons_kid_5_x 0.0)))
 (let (($x870 (>= buttons_kid_4_hight 0.0)))
 (let (($x869 (>= buttons_kid_4_width 0.0)))
 (let (($x868 (>= buttons_kid_4_y 0.0)))
 (let (($x867 (>= buttons_kid_4_x 0.0)))
 (let (($x866 (>= buttons_kid_3_hight 0.0)))
 (let (($x865 (>= buttons_kid_3_width 0.0)))
 (let (($x864 (>= buttons_kid_3_y 0.0)))
 (let (($x863 (>= buttons_kid_3_x 0.0)))
 (let (($x862 (>= buttons_kid_2_hight 0.0)))
 (let (($x861 (>= buttons_kid_2_width 0.0)))
 (let (($x860 (>= buttons_kid_2_y 0.0)))
 (let (($x859 (>= buttons_kid_2_x 0.0)))
 (let (($x858 (>= buttons_kid_1_hight 0.0)))
 (let (($x857 (>= buttons_kid_1_width 0.0)))
 (let (($x856 (>= buttons_kid_1_y 0.0)))
 (let (($x855 (>= buttons_kid_1_x 0.0)))
 (let (($x854 (>= buttons_kid_0_hight 0.0)))
 (let (($x853 (>= buttons_kid_0_width 0.0)))
 (let (($x852 (>= buttons_kid_0_y 0.0)))
 (let (($x851 (>= buttons_kid_0_x 0.0)))
 (let (($x850 (>= search_bar_kid_0_width 50.0)))
 (let (($x849 (= search_bar_kid_1_width 50.0)))
 (let ((?x847 (- (+ (- search_bar_kid_1_y search_bar_hight) search_bar_kid_1_hight) search_bar_y)))
 (let (($x848 (= ?x847 0.0)))
 (let ((?x842 (+ (+ (- search_bar_hight) search_bar_kid_0_y) search_bar_kid_0_hight)))
 (let (($x844 (= (- ?x842 search_bar_y) 0.0)))
 (let (($x840 (= (- search_bar_kid_1_y search_bar_y) 0.0)))
 (let (($x838 (= (- search_bar_kid_0_y search_bar_y) 0.0)))
 (let ((?x835 (+ (- (+ (- search_bar_x) search_bar_kid_1_x) search_bar_width) search_bar_kid_1_width)))
 (let (($x836 (= ?x835 0.0)))
 (let (($x832 (= (+ (- search_bar_x) search_bar_kid_0_x) 0.0)))
 (let (($x830 (= (- (- search_bar_kid_1_x search_bar_kid_0_x) search_bar_kid_0_width) 0.0)))
 (let (($x827 (>= search_bar_kid_1_hight 0.0)))
 (let (($x826 (>= search_bar_kid_1_width 0.0)))
 (let (($x825 (>= search_bar_kid_1_y 0.0)))
 (let (($x824 (>= search_bar_kid_1_x 0.0)))
 (let (($x823 (>= search_bar_kid_0_hight 0.0)))
 (let (($x822 (>= search_bar_kid_0_width 0.0)))
 (let (($x821 (>= search_bar_kid_0_y 0.0)))
 (let (($x820 (>= search_bar_kid_0_x 0.0)))
 (let (($x819 (= search_kid_6_width 80.0)))
 (let (($x818 (= search_kid_5_width 80.0)))
 (let (($x817 (= search_kid_4_width 50.0)))
 (let (($x815 (= search_kid_3_width 80.0)))
 (let (($x814 (= search_kid_1_width 80.0)))
 (let (($x813 (= search_kid_0_width 80.0)))
 (let (($x811 (= search_hight 70.0)))
 (let ((?x802 (- (+ (- search_kid_5_x) search_kid_6_x) search_kid_5_width)))
 (let (($x809 (= ?x802 10.0)))
 (let ((?x798 (- (+ (- search_kid_4_width) search_kid_5_x) search_kid_4_x)))
 (let (($x808 (= ?x798 10.0)))
 (let ((?x794 (+ (- (- search_kid_3_x) search_kid_3_width) search_kid_4_x)))
 (let (($x807 (= ?x794 10.0)))
 (let ((?x790 (- (+ (- search_bar_x) search_kid_3_x) search_bar_width)))
 (let (($x806 (= ?x790 10.0)))
 (let ((?x786 (- (- search_bar_x search_kid_1_x) search_kid_1_width)))
 (let (($x805 (= ?x786 10.0)))
 (let ((?x783 (- (- search_kid_1_x search_kid_0_x) search_kid_0_width)))
 (let (($x804 (= ?x783 10.0)))
 (let (($x803 (>= ?x802 0.0)))
 (let (($x799 (>= ?x798 0.0)))
 (let (($x795 (>= ?x794 0.0)))
 (let (($x791 (>= ?x790 0.0)))
 (let (($x787 (>= ?x786 0.0)))
 (let (($x784 (>= ?x783 0.0)))
 (let ((?x780 (- (+ (- search_y search_kid_6_y) search_hight) search_kid_6_hight)))
 (let (($x781 (>= ?x780 10.0)))
 (let ((?x607 (- search_y)))
 (let ((?x674 (+ ?x607 search_kid_6_y)))
 (let (($x777 (>= ?x674 10.0)))
 (let ((?x775 (- (+ (- search_width search_kid_6_width) search_x) search_kid_6_x)))
 (let (($x776 (>= ?x775 10.0)))
 (let (($x772 (>= (+ (- search_x) search_kid_6_x) 10.0)))
 (let ((?x769 (+ (- (+ (- search_kid_5_y) search_y) search_kid_5_hight) search_hight)))
 (let (($x770 (>= ?x769 10.0)))
 (let ((?x672 (- search_kid_5_y search_y)))
 (let (($x765 (>= ?x672 10.0)))
 (let ((?x763 (- (+ (- search_width search_kid_5_x) search_x) search_kid_5_width)))
 (let (($x764 (>= ?x763 10.0)))
 (let (($x760 (>= (- search_kid_5_x search_x) 10.0)))
 (let ((?x757 (- (+ (- search_y search_kid_4_y) search_hight) search_kid_4_hight)))
 (let (($x758 (>= ?x757 10.0)))
 (let ((?x670 (+ ?x607 search_kid_4_y)))
 (let (($x754 (>= ?x670 10.0)))
 (let ((?x752 (- (+ (- search_width search_kid_4_width) search_x) search_kid_4_x)))
 (let (($x753 (>= ?x752 10.0)))
 (let (($x749 (>= (+ (- search_x) search_kid_4_x) 10.0)))
 (let ((?x745 (- (+ (+ (- search_kid_3_hight) search_y) search_hight) search_kid_3_y)))
 (let (($x746 (>= ?x745 10.0)))
 (let ((?x668 (+ ?x607 search_kid_3_y)))
 (let (($x741 (>= ?x668 10.0)))
 (let ((?x739 (+ (- (- search_width search_kid_3_x) search_kid_3_width) search_x)))
 (let (($x740 (>= ?x739 10.0)))
 (let (($x736 (>= (- search_kid_3_x search_x) 10.0)))
 (let ((?x733 (- (+ (+ (- search_bar_hight) search_y) search_hight) search_bar_y)))
 (let (($x734 (>= ?x733 10.0)))
 (let ((?x666 (+ ?x607 search_bar_y)))
 (let (($x729 (>= ?x666 10.0)))
 (let (($x728 (>= (+ (- (- search_width search_bar_x) search_bar_width) search_x) 10.0)))
 (let (($x724 (>= (- search_bar_x search_x) 10.0)))
 (let ((?x721 (+ (+ (- (- search_kid_1_y) search_kid_1_hight) search_y) search_hight)))
 (let (($x722 (>= ?x721 10.0)))
 (let ((?x664 (- search_kid_1_y search_y)))
 (let (($x717 (>= ?x664 10.0)))
 (let ((?x715 (+ (- (- search_width search_kid_1_x) search_kid_1_width) search_x)))
 (let (($x716 (>= ?x715 10.0)))
 (let (($x712 (>= (- search_kid_1_x search_x) 10.0)))
 (let ((?x709 (+ (- (+ (- search_kid_0_y) search_y) search_kid_0_hight) search_hight)))
 (let (($x710 (>= ?x709 10.0)))
 (let ((?x662 (- search_kid_0_y search_y)))
 (let (($x705 (>= ?x662 10.0)))
 (let ((?x703 (- (+ (- search_width search_kid_0_x) search_x) search_kid_0_width)))
 (let (($x704 (>= ?x703 10.0)))
 (let ((?x654 (- search_kid_0_x search_x)))
 (let (($x700 (>= ?x654 10.0)))
 (let (($x699 (= (+ (- ?x674 search_hight) search_kid_6_hight) (- 10.0))))
 (let (($x696 (= (- (+ ?x672 search_kid_5_hight) search_hight) (- 10.0))))
 (let (($x693 (= (+ (- ?x670 search_hight) search_kid_4_hight) (- 10.0))))
 (let ((?x689 (+ (- (- search_kid_3_hight search_y) search_hight) search_kid_3_y)))
 (let (($x690 (= ?x689 (- 10.0))))
 (let (($x686 (= (+ (- (- search_bar_hight search_y) search_hight) search_bar_y) (- 10.0))))
 (let ((?x681 (- (- (+ search_kid_1_y search_kid_1_hight) search_y) search_hight)))
 (let (($x682 (= ?x681 (- 10.0))))
 (let (($x678 (= (- (+ ?x662 search_kid_0_hight) search_hight) (- 10.0))))
 (let (($x675 (= ?x674 10.0)))
 (let (($x673 (= ?x672 10.0)))
 (let (($x671 (= ?x670 10.0)))
 (let (($x669 (= ?x668 10.0)))
 (let (($x667 (= ?x666 10.0)))
 (let (($x665 (= ?x664 10.0)))
 (let (($x663 (= ?x662 10.0)))
 (let ((?x659 (+ (- (+ (- search_width) search_kid_6_width) search_x) search_kid_6_x)))
 (let (($x661 (= ?x659 (- 10.0))))
 (let (($x656 (= ?x654 10.0)))
 (let (($x653 (>= search_kid_6_hight 0.0)))
 (let (($x652 (>= search_kid_6_width 0.0)))
 (let (($x651 (>= search_kid_6_y 0.0)))
 (let (($x650 (>= search_kid_6_x 0.0)))
 (let (($x649 (>= search_kid_5_hight 0.0)))
 (let (($x648 (>= search_kid_5_width 0.0)))
 (let (($x647 (>= search_kid_5_y 0.0)))
 (let (($x646 (>= search_kid_5_x 0.0)))
 (let (($x645 (>= search_kid_4_hight 0.0)))
 (let (($x644 (>= search_kid_4_width 0.0)))
 (let (($x643 (>= search_kid_4_y 0.0)))
 (let (($x642 (>= search_kid_4_x 0.0)))
 (let (($x641 (>= search_kid_3_hight 0.0)))
 (let (($x640 (>= search_kid_3_width 0.0)))
 (let (($x639 (>= search_kid_3_y 0.0)))
 (let (($x638 (>= search_kid_3_x 0.0)))
 (let (($x637 (>= search_bar_hight 0.0)))
 (let (($x636 (>= search_bar_width 0.0)))
 (let (($x635 (>= search_bar_y 0.0)))
 (let (($x634 (>= search_bar_x 0.0)))
 (let (($x633 (>= search_kid_1_hight 0.0)))
 (let (($x632 (>= search_kid_1_width 0.0)))
 (let (($x631 (>= search_kid_1_y 0.0)))
 (let (($x630 (>= search_kid_1_x 0.0)))
 (let (($x629 (>= search_kid_0_hight 0.0)))
 (let (($x628 (>= search_kid_0_width 0.0)))
 (let (($x627 (>= search_kid_0_y 0.0)))
 (let (($x626 (>= search_kid_0_x 0.0)))
 (let (($x625 (= (+ (+ (- (- title_y) title_hight) buttons_y) buttons_hight) 0.0)))
 (let ((?x483 (- title_y)))
 (let ((?x589 (+ ?x483 search_y)))
 (let (($x621 (= ?x589 0.0)))
 (let (($x620 (= (+ (- (- buttons_width title_x) title_width) buttons_x) 0.0)))
 (let (($x616 (= (+ (- (- search_width title_x) title_width) search_x) 0.0)))
 (let ((?x476 (- title_x)))
 (let ((?x595 (+ ?x476 buttons_x)))
 (let (($x612 (= ?x595 0.0)))
 (let ((?x582 (+ ?x476 search_x)))
 (let (($x611 (= ?x582 0.0)))
 (let (($x610 (>= (- (+ ?x607 buttons_y) search_hight) 0.0)))
 (let (($x606 (>= (- (- (+ title_y title_hight) buttons_y) buttons_hight) 0.0)))
 (let (($x603 (>= (+ ?x483 buttons_y) 0.0)))
 (let (($x601 (>= (- (+ (+ (- buttons_width) title_x) title_width) buttons_x) 0.0)))
 (let (($x596 (>= ?x595 0.0)))
 (let (($x594 (>= (- (- (+ title_y title_hight) search_y) search_hight) 0.0)))
 (let (($x590 (>= ?x589 0.0)))
 (let (($x588 (>= (- (+ (+ (- search_width) title_x) title_width) search_x) 0.0)))
 (let (($x583 (>= ?x582 0.0)))
 (let (($x581 (>= buttons_hight 0.0)))
 (let (($x580 (>= buttons_width 0.0)))
 (let (($x579 (>= buttons_y 0.0)))
 (let (($x578 (>= buttons_x 0.0)))
 (let (($x577 (>= search_hight 0.0)))
 (let (($x576 (>= search_width 0.0)))
 (let (($x575 (>= search_y 0.0)))
 (let (($x574 (>= search_x 0.0)))
 (let (($x573 (= (- back_ground_y BC_y) 0.0)))
 (let (($x571 (= (+ (- (+ (- BC_width) back_ground_x) BC_x) back_ground_width) 0.0)))
 (let (($x566 (= (- back_ground_x BC_x) 0.0)))
 (let ((?x563 (+ (+ (- (- back_ground_y) back_ground_hight) info_y) info_hight)))
 (let (($x564 (= ?x563 0.0)))
 (let ((?x481 (- title_y back_ground_y)))
 (let (($x560 (= ?x481 0.0)))
 (let (($x559 (= (- (- (+ info_x info_width) back_ground_x) back_ground_width) 0.0)))
 (let ((?x554 (- (- (+ mainbody_x mainbody_width) back_ground_x) back_ground_width)))
 (let (($x555 (= ?x554 0.0)))
 (let (($x551 (= (- (+ (- ads_x back_ground_x) ads_width) back_ground_width) 0.0)))
 (let (($x548 (= (- (+ (- title_x back_ground_x) title_width) back_ground_width) 0.0)))
 (let ((?x517 (- info_x back_ground_x)))
 (let (($x545 (= ?x517 0.0)))
 (let ((?x502 (- mainbody_x back_ground_x)))
 (let (($x544 (= ?x502 0.0)))
 (let ((?x488 (- ads_x back_ground_x)))
 (let (($x543 (= ?x488 0.0)))
 (let ((?x474 (- title_x back_ground_x)))
 (let (($x542 (= ?x474 0.0)))
 (let ((?x537 (- (+ (- mainbody_hight) info_y) mainbody_y)))
 (let (($x541 (= ?x537 0.0)))
 (let ((?x534 (+ (- (- ads_y) ads_hight) mainbody_y)))
 (let (($x540 (= ?x534 0.0)))
 (let ((?x531 (- (+ ?x483 ads_y) title_hight)))
 (let (($x539 (= ?x531 0.0)))
 (let (($x538 (>= ?x537 0.0)))
 (let (($x535 (>= ?x534 0.0)))
 (let (($x532 (>= ?x531 0.0)))
 (let (($x529 (>= (- (- (+ back_ground_y back_ground_hight) info_y) info_hight) 0.0)))
 (let (($x525 (>= (+ (- back_ground_y) info_y) 0.0)))
 (let ((?x522 (+ (+ (- (- info_x) info_width) back_ground_x) back_ground_width)))
 (let (($x523 (>= ?x522 0.0)))
 (let (($x518 (>= ?x517 0.0)))
 (let ((?x515 (- (+ (+ (- mainbody_hight) back_ground_y) back_ground_hight) mainbody_y)))
 (let (($x516 (>= ?x515 0.0)))
 (let (($x511 (>= (+ (- back_ground_y) mainbody_y) 0.0)))
 (let (($x508 (>= (+ (+ (- ?x504 mainbody_width) back_ground_x) back_ground_width) 0.0)))
 (let (($x503 (>= ?x502 0.0)))
 (let (($x501 (>= (+ (- (+ (- ads_y) back_ground_y) ads_hight) back_ground_hight) 0.0)))
 (let (($x496 (>= (- ads_y back_ground_y) 0.0)))
 (let (($x494 (>= (+ (- (+ ?x490 back_ground_x) ads_width) back_ground_width) 0.0)))
 (let (($x489 (>= ?x488 0.0)))
 (let (($x487 (>= (+ (- (+ ?x483 back_ground_y) title_hight) back_ground_hight) 0.0)))
 (let (($x482 (>= ?x481 0.0)))
 (let (($x480 (>= (+ (- (+ ?x476 back_ground_x) title_width) back_ground_width) 0.0)))
 (let (($x475 (>= ?x474 0.0)))
 (let (($x473 (>= info_hight 0.0)))
 (let (($x472 (>= info_width 0.0)))
 (let (($x471 (>= info_y 0.0)))
 (let (($x470 (>= info_x 0.0)))
 (let (($x469 (>= mainbody_hight 0.0)))
 (let (($x468 (>= mainbody_width 0.0)))
 (let (($x467 (>= mainbody_y 0.0)))
 (let (($x466 (>= mainbody_x 0.0)))
 (let (($x465 (>= ads_hight 0.0)))
 (let (($x464 (>= ads_width 0.0)))
 (let (($x463 (>= ads_y 0.0)))
 (let (($x462 (>= ads_x 0.0)))
 (let (($x461 (>= title_hight 0.0)))
 (let (($x460 (>= title_width 0.0)))
 (let (($x459 (>= title_y 0.0)))
 (let (($x458 (>= title_x 0.0)))
 (let (($x457 (>= back_ground_hight 0.0)))
 (let (($x456 (>= back_ground_width 0.0)))
 (let (($x455 (>= back_ground_y 0.0)))
 (let (($x454 (>= back_ground_x 0.0)))
 (let (($x453 (= BC_y 0.0)))
 (let (($x452 (= BC_x 0.0)))
 (let (($x451 (<= BC_width 4000.0)))
 (let (($x449 (>= BC_hight 0.0)))
 (let (($x448 (>= BC_width 0.0)))
 (let (($x447 (>= BC_y 0.0)))
 (let (($x446 (>= BC_x 0.0)))
 (and $x446 $x447 $x448 $x449 $x451 $x452 $x453 BC_feasible $x454 $x455 $x456 $x457 $x458 $x459 $x460 $x461 $x462 $x463 $x464 $x465 $x466 $x467 $x468 $x469 $x470 $x471 $x472 $x473 $x475 $x480 $x482 $x487 $x489 $x494 $x496 $x501 $x503 $x508 $x511 $x516 $x518 $x523 $x525 $x529 $x532 $x535 $x538 $x539 $x540 $x541 $x542 $x543 $x544 $x545 $x548 $x551 $x555 $x559 $x560 $x564 $x566 $x571 $x573 $x574 $x575 $x576 $x577 $x578 $x579 $x580 $x581 $x583 $x588 $x590 $x594 $x596 $x601 $x603 $x606 $x610 $x611 $x612 $x616 $x620 $x621 $x625 $x626 $x627 $x628 $x629 $x630 $x631 $x632 $x633 $x634 $x635 $x636 $x637 $x638 $x639 $x640 $x641 $x642 $x643 $x644 $x645 $x646 $x647 $x648 $x649 $x650 $x651 $x652 $x653 $x656 $x661 $x663 $x665 $x667 $x669 $x671 $x673 $x675 $x678 $x682 $x686 $x690 $x693 $x696 $x699 $x700 $x704 $x705 $x710 $x712 $x716 $x717 $x722 $x724 $x728 $x729 $x734 $x736 $x740 $x741 $x746 $x749 $x753 $x754 $x758 $x760 $x764 $x765 $x770 $x772 $x776 $x777 $x781 $x784 $x787 $x791 $x795 $x799 $x803 $x804 $x805 $x806 $x807 $x808 $x809 $x811 $x813 $x814 $x815 $x817 $x818 $x819 $x820 $x821 $x822 $x823 $x824 $x825 $x826 $x827 $x830 $x832 $x836 $x838 $x840 $x844 $x848 $x849 $x850 $x851 $x852 $x853 $x854 $x855 $x856 $x857 $x858 $x859 $x860 $x861 $x862 $x863 $x864 $x865 $x866 $x867 $x868 $x869 $x870 $x871 $x872 $x873 $x874 $x875 $x876 $x877 $x878 $x879 $x880 $x881 $x882 $x883 $x884 $x885 $x886 $x887 $x888 $x889 $x890 $x891 $x892 $x893 $x894 $x895 $x896 $x897 $x898 $x899 $x900 $x901 $x902 $x903 $x904 $x905 $x906 $x907 $x908 $x909 $x910 $x911 $x912 $x913 $x914 $x915 $x916 $x917 $x918 $x920 $x921 $x922 $x923 $x924 $x925 $x926 $x927 $x928 $x929 $x930 $x931 $x932 $x933 $x934 $x935 $x936 $x937 $x939 $x942 $x946 $x950 $x952 $x956 $x957 $x961 $x962 $x966 $x967 $x971 $x973 $x977 $x979 $x983 $x985 $x989 $x991 $x995 $x996 $x1000 $x1001 $x1005 $x1006 $x1010 $x1012 $x1016 $x1018 $x1022 $x1024 $x1027 $x1029 $x1033 $x1034 $x1038 $x1042 $x1046 $x1050 $x1054 $x1058 $x1062 $x1066 $x1070 $x1074 $x1078 $x1082 $x1086 $x1090 $x1094 $x1098 $x1104 $x1106 $x1112 $x1114 $x1120 $x1122 $x1128 $x1130 $x1136 $x1138 $x1144 $x1146 $x1152 $x1154 $x1160 $x1162 $x1168 $x1170 $x1176 $x1178 $x1184 $x1186 $x1192 $x1194 $x1200 $x1202 $x1208 $x1210 $x1216 $x1218 $x1224 $x1226 $x1232 $x1234 $x1235 $x1236 $x1237 $x1238 $x1239 $x1240 $x1241 $x1242 $x1244 $x1248 $x1250 $x1254 $x1256 $x1260 $x1262 $x1266 $x1270 $x1271 $x1272 $x1273 $x1274 $x1275 $x1276 $x1277 $x1278 $x1279 $x1280 $x1281 $x1282 $x1287 $x1291 $x1294 $x1298 $x1302 $x1306 $x1310 $x1315 $x1319 $x1324 $x1327 $x1332 $x1333 $x1334 $x1335 $x1336 $x1338 $x1342 $x1347 $x1348 $x1349 $x1350 $x1351 $x1352 $x1353 $x1354 $x1355 $x1356 $x1357 $x1358 $x1359 $x1362 $x1368 $x1372 $x1377 $x1381 $x1387 $x1390 $x1394 $x1397 $x1402 $x1405 $x1410 $x1414 $x1418 $x1425 $x1428 $x1430 $x1432 $x1438 $x1442 $x1445 $x1448 $x1454 $x1457 $x1460 $x1462 $x1465 $x1470 $x1473 $x1478 $x1482 $x1487 $x1490 $x1495 $x1496 $x1498 $x1500 $x1502 $x1508 $x1509 $x1510 $x1511 $x1512 $x1513 $x1514 $x1515 $x1516 $x1520 $x1524 $x1527 $x1531 $x1535 $x1539 $x1542 $x1546 $x1547 $x1548 $x1549 $x1550 $x1551 $x1552 $x1553 $x1554 $x1555 $x1556 $x1557 $x1558 $x1559 $x1560 $x1561 $x1562 $x1563 $x1564 $x1565 $x1566 $x1567 $x1568 $x1571 $x1577 $x1581 $x1584 $x1587 $x1590 $x1593 $x1598 $x1603 $x1607 $x1611 $x1615 $x1619 $x1624 $x1629 $x1634 $x1636 $x1642 $x1644 $x1649 $x1652 $x1657 $x1659 $x1664 $x1667 $x1671 $x1673 $x1677 $x1680 $x1685 $x1687 $x1692 $x1694 $x1699 $x1701 $x1706 $x1708 $x1710 $x1712 $x1714 $x1721 $x1722 $x1726 $x1730 $x1733 $x1736 $x1738 $x1739 $x1740 $x1741 $x1742 $x1743 $x1744 $x1745 $x1746 $x1749 $x1755 $x1758 $x1764 $x1767 $x1773 $x1776 $x1782 $x1786 $x1787 $x1789 $x1791 $x1795 $x1799 $x1801 $x1805 $x1807 $x1811 $x1813 $x1816 $x1817 $x1818 $x1819 $x1820 $x1821 $x1822 $x1823 $x1824 $x1828 $x1834 $x1837 $x1842 $x1845 $x1851 $x1854 $x1859 $x1863 $x1865 $x1870 $x1872 $x1877 $x1879 $x1886 $x1889 $x1891 $x1892 $x1893 $x1894 $x1895 $x1896 $x1897 $x1898 $x1899 $x1900 $x1901 $x1902 $x1903 $x1904 $x1905 $x1906 $x1907 $x1911 $x1917 $x1920 $x1925 $x1928 $x1934 $x1937 $x1941 $x1944 $x1949 $x1952 $x1957 $x1960 $x1966 $x1969 $x1973 $x1977 $x1981 $x1985 $x1988 $x1991 $x1994 $x1996 $x1998 $x2003 $x2005 $x2009 $x2011 $x2015 $x2017 $x2021 $x2023 $x2025 $x2027 $x2029 $x2030 $x2031 $x2032 $x2033 $x2034 $x2035 $x2036 $x2037 $x2038 $x2039 $x2040 $x2041 $x2046 $x2050 $x2052 $x2054 $x2056 $x2060 $x2063 $x2067 $x2069 $x2073 $x2074 $x2078 $x2079 $x2083 $x2084 $x2089 $x2091 $x2095 $x2096 $x2101 $x2103 $x2107 $x2108 $x2109 $x2111 $x2113 $x2115 $x2116 $x2117 $x2118 $x2119 $x2120 $x2121 $x2122 $x2123 $x2126 $x2129 $x2134 $x2136 $x2140 $x2142 $x2147 $x2149 $x2152 $x2153 $x2154 $x2155 $x2156 $x2159 $x2162 $x2165 $x2166 $x2167 $x2168 $x2169 $x2170 $x2171 $x2172 $x2173 $x2174 $x2175 $x2176 $x2177 $x2178 $x2179 $x2180 $x2181 $x2182 $x2183 $x2184 $x2185 $x2186 $x2187 $x2188 $x2189 $x2190 $x2191 $x2192 $x2193 $x2195 $x2196 $x2197 $x2198 $x2199 $x2200 $x2201 $x2205 $x2207 $x2209 $x2212 $x2217 $x2219 $x2223 $x2225 $x2229 $x2231 $x2235 $x2236 $x2240 $x2241 $x2245 $x2246 $x2250 $x2254 $x2258 $x2262 $x2266 $x2270 $x2276 $x2278 $x2284 $x2286 $x2292 $x2294 $x2300 $x2302 $x2308 $x2310 $x2316 $x2318 $x2324 $x2326 $x2327 $x2328 $x2329 $x2330 $x2331 $x2332 $x2333 $x2334 $x2338 $x2340 $x2344 $x2346 $x2350 $x2352 $x2356 $x2359 $x2363 $x2364 $x2365 $x2366 $x2367 $x2371 $x2373 $x2375 $x2376 $x2377 $x2378 $x2379 $x2380 $x2381 $x2382 $x2383 $x2384 $x2385 $x2386 $x2387 $x2388 $x2389 $x2390 $x2391 $x2392 $x2393 $x2394 $x2395 $x2396 $x2397 $x2398 $x2399 $x2400 $x2401 $x2402 $x2403 $x2404 $x2405 $x2406 $x2407 $x2408 $x2409 $x2410 $x2413 $x2416 $x2418 $x2422 $x2426 $x2428 $x2433 $x2435 $x2439 $x2441 $x2445 $x2447 $x2451 $x2453 $x2457 $x2460 $x2464 $x2468 $x2472 $x2476 $x2480 $x2484 $x2489 $x2491 $x2497 $x2499 $x2505 $x2507 $x2513 $x2515 $x2521 $x2523 $x2528 $x2530 $x2536 $x2538 $x2539 $x2540 $x2541 $x2542 $x2543 $x2544 $x2545 $x2546 $x2550 $x2552 $x2555 $x2558 $x2562 $x2564 $x2568 $x2570 $x2574 $x2575 $x2576 $x2577 $x2578 $x2581 $x2583 $x2585 $x2586 $x2587 $x2588 $x2589 $x2590 $x2591 $x2592 $x2593 $x2594 $x2595 $x2596 $x2597 $x2598 $x2599 $x2600 $x2601 $x2602 $x2603 $x2604 $x2605 $x2606 $x2607 $x2608 $x2609 $x2610 $x2611 $x2612 $x2613 $x2614 $x2615 $x2616 $x2617 $x2618 $x2619 $x2620 $x2623 $x2626 $x2628 $x2631 $x2635 $x2636 $x2640 $x2642 $x2646 $x2648 $x2652 $x2655 $x2659 $x2661 $x2665 $x2666 $x2670 $x2674 $x2678 $x2682 $x2686 $x2690 $x2696 $x2698 $x2704 $x2706 $x2712 $x2714 $x2719 $x2721 $x2727 $x2729 $x2734 $x2736 $x2742 $x2744 $x2745 $x2746 $x2747 $x2748 $x2750 $x2754 $x2756 $x2761 $x2762 $x2765 $x2766 $x2772 $x2773 back_ground_feasible title_feasible ads_feasible mainbody_feasible info_feasible search_feasible buttons_feasible search_kid_0_feasible search_kid_1_feasible search_bar_feasible search_kid_3_feasible search_kid_4_feasible search_kid_5_feasible search_kid_6_feasible search_bar_kid_0_feasible search_bar_kid_1_feasible ads_top_holder_feasible ads_pics_holder_feasible $x2774 $x2775 $x2777 $x2778 $x2779 $x2780 $x2782 $x2783 $x2785 $x2786 $x2788 $x2789 $x2791 $x2792 $x2794 $x2795 $x2797 $x2798 $x2800 $x2801 $x2802 $x2803 $x2804 $x2805 $x2807 $x2808 $x2810 $x2811 $x2813 $x2814 $x2816 $x2817 $x2819 $x2820 $x2822 $x2823 video_1_feasible video_2_feasible video_3_feasible video_1_title_feasible video_1_body_feasible video_2_title_feasible video_2_body_feasible video_3_title_feasible video_3_body_feasible back_to_top_feasible)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)

